Commit 284b03aa authored by Jean-Christophe's avatar Jean-Christophe

programs: fixed bug with global references

parent a1d7fd72
......@@ -165,9 +165,9 @@ programs bench/programs/good
# programs examples/programs
echo ""
# echo "=== Checking valid goals ===" *)
# valid_goals bench/valid *)
# echo "" *)
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== Checking provers ==="
echo -n "Test provers on true..."
......
......@@ -1495,8 +1495,7 @@ let type_type uc ty =
let dty = Typing.dty denv.denv ty in
Denv.ty_of_dty dty
let add_logic_decl uc loc id ty =
let ls = create_lsymbol id [] (Some ty) in
let add_logic_decl uc loc ls =
try
Pgm_module.add_logic_decl (Decl.create_logic_decl [ls, None]) uc
with Theory.ClashSymbol _ ->
......@@ -1509,13 +1508,11 @@ let add_global loc x tyv uc =
with Pgm_module.ClashSymbol _ ->
errorm ~loc "clash with previous symbol %s" x
let add_global_if_pure gl { p_ls = ls } = match ls.ls_args, ls.ls_value with
| [], Some { ty_node = Ty.Tyapp (ts, _) } when ts_equal ts ts_arrow ->
let add_global_if_pure gl { p_ls = ls; p_ty = ty } = match ty with
| { ty_node = Ty.Tyapp (ts, _) } when ts_equal ts ts_arrow ->
gl
| [], Some ty ->
let ty = purify ty in
add_logic_decl gl (loc_of_ls ls) (id_dup ls.ls_name) ty
| _ -> gl
| _ ->
add_logic_decl gl (loc_of_ls ls) ls
let add_exception loc x ty uc =
try
......
......@@ -264,10 +264,11 @@ let rec wp_expr env e q =
let f = wp_desc env e q in
let f = erase_label env lab f in
let f = propose_label (label ~loc:e.expr_loc "WP") f in
if Debug.test_flag debug then
eprintf "@[--------@\n@[<hov 2>e = %a@]@\n@[<hov 2>q = %a@]@\n----@]@."
Pgm_pretty.print_expr e
Pretty.print_fmla (snd (fst q));
if Debug.test_flag debug then begin
eprintf "@[--------@\n@[<hov 2>e = %a@]@\n" Pgm_pretty.print_expr e;
eprintf "@[<hov 2>q = %a@]@\n" Pretty.print_fmla (snd (fst q));
eprintf "@[<hov 2>f = %a@]@\n----@]@\n" Pretty.print_fmla f;
end;
f
and wp_desc env e q = match e.expr_desc with
......
......@@ -4,18 +4,11 @@ module P
use import int.Int
use import module stdlib.Ref
(* parameter b : ref int *)
(* let f () = *)
(* { b>0 } !b + 1 { result > b } *)
let test r =
{ r = 1 }
assert { r = 1 };
r := !r + 1;
assert { r = 2 }
{ true }
(* let create sz = *)
(* { 0 <= sz <= maxlen } *)
(* ref (SA (malloc sz) (malloc sz) (malloc sz) sz 0) *)
(* { invariant_ result and *)
(* sa_sz result = sz and forall i:int. model result i = default } *)
end
(*
......
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