Commit ffd0d006 authored by David Hauzar's avatar David Hauzar
Browse files

Merge branch 'counter-examples'

parents 1779f110 763d4d0d
......@@ -31,7 +31,7 @@ type model_value =
| Integer of string
| Decimal of (string * string)
| Array of model_array
| Bitvector of int
| Bitvector of string
| Unparsed of string
and arr_index = {
arr_index_key : model_value;
......@@ -87,7 +87,7 @@ print_model_value_sanit sanit_print fmt value =
| Array a ->
print_array str_formatter a;
sanit_print fmt (flush_str_formatter ())
| Bitvector v -> sanit_print fmt (string_of_int v)
| Bitvector v -> sanit_print fmt v
and
print_model_value fmt value =
print_model_value_sanit (fun fmt s -> fprintf fmt "%s" s) fmt value
......
......@@ -18,7 +18,7 @@ type model_value =
| Integer of string
| Decimal of (string * string)
| Array of model_array
| Bitvector of int
| Bitvector of string
| Unparsed of string
and arr_index = {
arr_index_key : model_value;
......
......@@ -20,7 +20,7 @@ rule token = parse
{ LPAREN }
| ')'
{ RPAREN }
| "(_ bv"(num as bv_value)" "num")" { BITVECTOR_VALUE (int_of_string bv_value) }
| "(_ bv"(num as bv_value)" "num")" { BITVECTOR_VALUE bv_value }
| num as integer
{ INT_STR (integer) }
| '-'space*(num as integer) { MINUS_INT_STR ("-"^integer) }
......
......@@ -7,7 +7,7 @@
%token STORE
%token CONST
%token AS
%token <int> BITVECTOR_VALUE
%token <string> BITVECTOR_VALUE
%token <string> INT_STR
%token <string> MINUS_INT_STR
%token <string * string> DEC_STR
......
......@@ -119,8 +119,12 @@ let default_post vty ef =
let vs = create_vsymbol (id_fresh "result") (ty_of_vty vty) in
create_post vs t_true, Mexn.mapi default_exn_post ef.eff_raises
let wp_label e f =
let loc = if f.t_loc = None then e.e_loc else f.t_loc in
let wp_label ?(override=false) e f =
let loc =
if e.e_loc = None then f.t_loc
else if f.t_loc = None then e.e_loc
else if override then e.e_loc else f.t_loc
in
let lab = Ident.Slab.union e.e_label f.t_label in
t_label ?loc lab f
......@@ -1627,8 +1631,10 @@ and fast_wp_desc (env : wp_env) (s : Subst.t) (r : res_type) (e : expr)
let call_regs = regs_of_writes spec.c_effect in
let pre_call_label = fresh_mark () in
let state_before_call = Subst.save_label pre_call_label wp1.post.s in
let pre = wp_label e (Subst.term state_before_call spec.c_pre) in
let md = create_model_data_opt ~loc:e1.e_loc ~context_labels:e1.e_label "call" in
let pre =
wp_label ~override:true e (Subst.term state_before_call spec.c_pre) in
let md =
create_model_data_opt ~loc:e1.e_loc ~context_labels:e1.e_label "call" in
let state_after_call, call_glue =
Subst.havoc md env call_regs state_before_call in
let xpost = Mexn.map (fun p ->
......
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