Commit 8c6d96ee authored by David Hauzar's avatar David Hauzar

Merge branch 'counter-examples'

parents d0fdf426 e8a8118d
......@@ -65,6 +65,11 @@ module M
=
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let test_map2 (x "model" : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
type r = {f:int; g:bool}
let test_record1 (x "model" "model_trace:x" : r) : int
......
......@@ -30,6 +30,7 @@ let debug = Debug.register_info_flag "model_parser"
type model_value =
| Integer of string
| Array of model_array
| Bitvector of int
| Unparsed of string
and arr_index = {
arr_index_key : int;
......@@ -82,6 +83,7 @@ print_model_value_sanit sanit_print fmt value =
| Integer s -> sanit_print fmt s
| Unparsed s -> sanit_print fmt s
| Array a -> print_array sanit_print fmt a
| Bitvector v -> sanit_print fmt (string_of_int v)
let print_model_value fmt value =
print_model_value_sanit (fun fmt s -> fprintf fmt "%s" s) fmt value
......
......@@ -17,6 +17,7 @@
type model_value =
| Integer of string
| Array of model_array
| Bitvector of int
| Unparsed of string
and arr_index = {
arr_index_key : int;
......
......@@ -5,6 +5,7 @@
let atom = [^'('')'' ''\t''\n']
let space = [' ''\t''\n']
let num = ['0'-'9']+
rule token = parse
| '\n'
......@@ -18,8 +19,9 @@ rule token = parse
{ LPAREN }
| ')'
{ RPAREN }
| ['0'-'9']+ as integer
| num as integer
{ INT_STR (integer) }
| "(_ bv"(num as bv_value)" "num")" { BITVECTOR_VALUE (int_of_string bv_value) }
| '-'space*(['0'-'9']+ as integer) { MINUS_INT_STR ("-"^integer) }
| atom+ as at { ATOM (at) }
| eof
......@@ -27,4 +29,3 @@ rule token = parse
(* | space { SPACE } *)
| _
{ raise SyntaxError }
......@@ -2,13 +2,13 @@
%}
%start <Model_parser.model_element list> output
%token <string> SPACE
%token <string> ATOM
%token STORE
%token CONST
%token AS
%token <string> INT_STR
%token <int> BITVECTOR_VALUE
%token <string> MINUS_INT_STR
%token LPAREN RPAREN
%token EOF
......@@ -54,6 +54,7 @@ value:
| integer { $1 }
| other_val_str { Model_parser.Unparsed $1 }
| array { Model_parser.Array $1 }
| bitvector { Model_parser.Bitvector $1 }
integer:
| INT_STR { Model_parser.Integer $1 }
......@@ -85,20 +86,27 @@ other_than_const_array:
| CONST { "const" }
(* Example:
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4) *)
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4)
(store (store ((as const (Array Int Int)) false) 1 true) 3 true) *)
array:
| LPAREN possible_space
LPAREN possible_space
AS SPACE CONST possible_space array_skipped_part possible_space
RPAREN possible_space
integer possible_space
value possible_space
RPAREN
{ Model_parser.array_create_constant ~value:$13 }
| LPAREN possible_space
STORE possible_space array possible_space integer SPACE integer
STORE possible_space array possible_space value SPACE integer
possible_space
RPAREN
{ Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
(* Example:
(_ bv2048 16) *)
bitvector:
| BITVECTOR_VALUE
{ $1 }
array_skipped_part:
| LPAREN term_list RPAREN {}
......@@ -643,10 +643,13 @@ let update_tabs a =
match a.S.proof_state with
| S.Done r ->
if not (Model_parser.is_model_empty r.Call_provers.pr_model) then begin
Model_parser.interleave_with_source
r.Call_provers.pr_model
~filename:!current_file
~source_code:(Sysutil.file_contents !current_file)
"Counterexample:\n" ^
(Model_parser.model_to_string r.Call_provers.pr_model) ^
"\n\nSource code interleaved with counterexample:" ^
(Model_parser.interleave_with_source
r.Call_provers.pr_model
~filename:!current_file
~source_code:(Sysutil.file_contents !current_file))
end else
""
| _ -> ""
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment