diff --git a/bench/bench b/bench/bench
index f967d0c5286870576268e16f01d09395df0a7017..17871da32bf2240c2b760de6a316467b6f3af6b3 100755
--- a/bench/bench
+++ b/bench/bench
@@ -196,6 +196,7 @@ echo ""
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
+goods bench/ce
goods examples/bts
goods examples/tests
goods examples/tests-provers
diff --git a/bench/ce/int_overflow.mlw b/bench/ce/int_overflow.mlw
index f359b04c2db0619d3fe19acf5bd2340b4759e15e..8f53a7bab6654cf5dcdb8f64cd680e727e407be0 100644
--- a/bench/ce/int_overflow.mlw
+++ b/bench/ce/int_overflow.mlw
@@ -3,59 +3,59 @@ theory ModelInt
use import int.Int
(* PASS *)
-goal test0 : forall x "model":int. not (0 < x < 1)
+goal test0 : forall x [@model]:int. not (0 < x < 1)
(* CE *)
-goal test1 : forall x "model":int. not (0 <= x <= 1)
+goal test1 : forall x [@model]:int. not (0 <= x <= 1)
use import int.EuclideanDivision
(* CE *)
-goal test2 : forall x "model":int. div x x = 1
+goal test2 : forall x [@model]:int. div x x = 1
(* CE *)
goal test_overflow:
- forall x "model" y "model" : int.
+ forall x [@model] y [@model] : int.
0 <= x <= 65535 /\ 0 <= y <= 65535 -> 0 <= x + y <= 65535
(* CE *)
goal test_overflow2:
- forall x "model" y "model" : int.
+ forall x [@model] y [@model] : int.
-2 <= x <= 65535 /\ -2 <= y <= 65535 -> -2 <= x + y <= 65535
predicate is_int16 (x:int) = -65536 <= x <= 65535
(* CE *)
goal test_overflow_int16:
- forall x "model" y "model" : int.
+ forall x [@model] y [@model] : int.
is_int16 x /\ is_int16 y -> is_int16 (x + y)
(* CE *)
goal test_overflow_int16_alt:
- forall x "model" y "model" : int.
+ forall x [@model] y [@model] : int.
-65536 <= x <= 65535 /\ -65536 <= y <= 65535 -> -65536 <= x+y <= 65535
(* CE *)
goal test_overflow_int16_bis:
- forall x "model" y "model" : int.
+ forall x [@model] y [@model] : int.
is_int16 x /\ is_int16 y /\
- ("model" 0 <= x) /\ (x <= y) -> is_int16 (x + y)
+ ([@model] 0 <= x) /\ (x <= y) -> is_int16 (x + y)
predicate is_int32 (x:int) = -2147483648 <= x <= 2147483647
(* CE *)
goal test_overflow_int32:
- forall x "model" y "model" : int.
+ forall x [@model] y [@model] : int.
is_int32 x /\ is_int32 y -> is_int32 (x + y)
(* CE *)
goal test_overflow_int32_bis:
- forall x "model" y "model" : int.
+ forall x [@model] y [@model] : int.
is_int32 x /\ is_int32 y /\ 0 <= x <= y -> is_int32 (x + y)
(* CE *)
goal test_overflow_int32_bis_inline:
- forall x "model" y "model" : int.
+ forall x [@model] y [@model] : int.
-2147483648 <= x <= 2147483647 /\ -2147483648 <= y <= 2147483647 /\ 0 <= x <= y -> -2147483648 <= x + y <= 2147483647
end
diff --git a/bench/ce/logic.mlw b/bench/ce/logic.mlw
index ac1e13a309c8eaf52b8dbc7dff82cd19794a80c6..8875421d853594148303f54b23fc39978947e234 100644
--- a/bench/ce/logic.mlw
+++ b/bench/ce/logic.mlw
@@ -3,21 +3,21 @@ theory T
use import int.Int
- goal g0 : forall x "model":int. ("model" x >= 42) -> ("model" x + 3 <= 50)
+ goal g0 : forall x [@model]:int. ([@model] x >= 42) -> ([@model] x + 3 <= 50)
constant g : int
- goal g1 : forall x "model":int. ("model" g >= x)
+ goal g1 : forall x [@model]:int. ([@model] g >= x)
- goal g2 : forall x1 "model" "model_trace:X" x2 "model" x3 "model" x4 "model" x5 "model" x6 "model" x7 "model" x8 "model".
- ("model" "model_trace: X1 + 1 = 2" x1 + 1 = 2) ->
- ("model" x2 + 1 = 2) ->
- ("model" x3 + 1 = 2) ->
- ("model" x4 + 1 = 2) ->
- ("model" x5 + 1 = 2) ->
- ("model" x6 + 1 = 2) ->
- ("model" x7 + 1 = 2) ->
- ("model" x8 + 1 = 2) ->
- ("model" x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
+ goal g2 : forall x1 [@model] [@model_trace:X] x2 [@model] x3 [@model] x4 [@model] x5 [@model] x6 [@model] x7 [@model] x8 [@model].
+ ([@model] [@model_trace: X1 + 1 = 2] x1 + 1 = 2) ->
+ ([@model] x2 + 1 = 2) ->
+ ([@model] x3 + 1 = 2) ->
+ ([@model] x4 + 1 = 2) ->
+ ([@model] x5 + 1 = 2) ->
+ ([@model] x6 + 1 = 2) ->
+ ([@model] x7 + 1 = 2) ->
+ ([@model] x8 + 1 = 2) ->
+ ([@model] x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
end
diff --git a/bench/ce/map.mlw b/bench/ce/map.mlw
index 6fe6bb06a040bf3010b7bc5b0afca374a8fcae19..33881b20de108e764bed961b8870f304fdd9f0c4 100644
--- a/bench/ce/map.mlw
+++ b/bench/ce/map.mlw
@@ -7,24 +7,24 @@ module M
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
- val y "model" "model_trace:Y" :ref int
+ val y [@model] [@model_trace:Y] :ref int
- let incr ( x23 "model" "model_trace:X2" : ref int ): unit
- ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
+ let incr ( x23 [@model] [@model_trace:X2] : ref int ): unit
+ ensures { [@model_vc_post] !x23 = old !x23 + 2 + !y }
=
(*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
y := !y + 1;
x23 := !x23 + 1;
x23 := !x23 + 1
- let test_loop ( x "model" "model_trace:x" : ref int ): unit
- ensures { "model_vc_post" !x < old !x }
+ let test_loop ( x [@model] [@model_trace:x] : ref int ): unit
+ ensures { [@model_vc_post] !x < old !x }
=
label L in
incr x;
label M in
while !x > 0 do
- invariant { "model_vc" !x > !x at L + !x at M }
+ invariant { [@model_vc] !x > !x at L + !x at M }
variant { !x }
x := !x - 1
done
diff --git a/bench/ce/real.mlw b/bench/ce/real.mlw
index 3f8b2655cd4fc1c7a38f29bcbc12882545322d70..fba5c19e04b45a4fffdb935b7f180c63c6d5a929 100644
--- a/bench/ce/real.mlw
+++ b/bench/ce/real.mlw
@@ -2,8 +2,8 @@ theory ModelReal
use import real.Real
-goal test1 : forall x "model":real. not (0.0 < x < 1.0)
+goal test1 : forall x [@model]:real. not (0.0 < x < 1.0)
-goal test2 : forall x "model":real. x/x=1.0
+goal test2 : forall x [@model]:real. x/x=1.0
end
diff --git a/bench/ce/records.mlw b/bench/ce/records.mlw
index b6e060636bba4276e6c3ff8a6242e5df77ee66c6..059ecf356184fecec79b6c242a2bc8d576243a36 100644
--- a/bench/ce/records.mlw
+++ b/bench/ce/records.mlw
@@ -10,13 +10,13 @@ module M
(*** In all cases, records are decomposed using match eval ***)
- type r = {f "model_trace:.field_f" :int; g:bool}
+ type r = {f [@model_trace:.field_f] :int; g:bool}
(* Projection functions *)
- function projf_r_f "model_trace:.f" (x : r) : int
+ function projf_r_f [@model_trace:.f] (x : r) : int
=
x.f
- function projf_r_g "model_trace:.g" (x : r) : bool
+ function projf_r_g [@model_trace:.g] (x : r) : bool
=
x.g
meta "inline:no" function projf_r_f
@@ -24,34 +24,34 @@ module M
meta "inline:no" function projf_r_g
meta "model_projection" function projf_r_g
- let record_match_eval_test1 (x "model" "model_trace:x" : r) : int
- ensures { "model_vc_post" result = 1 }
+ let record_match_eval_test1 (x [@model] [@model_trace:x] : r) : int
+ ensures { [@model_vc_post] result = 1 }
=
if x.g then
x.f
else
1
- let record_match_eval_test2 (x "model_projected" : r ) : int
+ let record_match_eval_test2 (x [@model_projected] : r ) : int
ensures { result = 1 }
=
x.f
- let record_match_eval_test3 (x "model" "model_trace:x" : ref r) : unit
+ let record_match_eval_test3 (x [@model] [@model_trace:x] : ref r) : unit
ensures { !x.g }
=
x := { !x with f = 6}
- let record_match_eval_test4 (x "model" "model_trace:x" : ref r) : r
- ensures { "model_vc_post" result.g }
+ let record_match_eval_test4 (x [@model] [@model_trace:x] : ref r) : r
+ ensures { [@model_vc_post] result.g }
=
x := { !x with f = 6 };
!x
- val re "model_projected" : ref r
+ val re [@model_projected] : ref r
- let test_record_match_eval_test5 (x "model" "model_trace:x" : ref r) : r
- ensures { "model_vc_post" result = !re }
+ let test_record_match_eval_test5 (x [@model] [@model_trace:x] : ref r) : r
+ ensures { [@model_vc_post] result = !re }
=
x := { !x with f = 6 };
!x
diff --git a/bench/ce/ref.mlw b/bench/ce/ref.mlw
index 529d4a8ea4865f95257d6680c4bfdbceeff6ffe7..c6e94396d912e4945e3c2dbf47f2d84cd1462373 100644
--- a/bench/ce/ref.mlw
+++ b/bench/ce/ref.mlw
@@ -5,34 +5,34 @@ module M
type int_type = Integer int
- goal G : forall x "model" : int_type. match x with Integer y -> y > 0 end
+ goal G : forall x [@model] : int_type. match x with Integer y -> y > 0 end
- let test_post (x "model" "model_trace:x" : int) (y "model" "model_trace:y" : ref int): unit
- ensures { "model_vc_post" old !y >= x }
+ let test_post (x [@model] [@model_trace:x] : int) (y [@model] [@model_trace:y] : ref int): unit
+ ensures { [@model_vc_post] old !y >= x }
=
y := x - 1 + !y
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
- val y "model" "model_trace:y" :ref int
+ val y [@model] [@model_trace:y] :ref int
- let incr ( x23 "model" "model_trace:x23" : ref int ): unit
- ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
+ let incr ( x23 [@model] [@model_trace:x23] : ref int ): unit
+ ensures { [@model_vc_post] !x23 = old !x23 + 2 + !y }
=
(*#"random_path.random" 62 27 32#*)
y := !y + 1;
x23 := !x23 + 1;
x23 := !x23 + 1
- let test_loop ( x "model" "model_trace:x" : ref int ): unit
- ensures { "model_vc_post" !x < old !x }
+ let test_loop ( x [@model] [@model_trace:x] : ref int ): unit
+ ensures { [@model_vc_post] !x < old !x }
=
label L in
incr x;
label M in
while !x > 0 do
- invariant { "model_vc" !x > !x at L + !x at M }
+ invariant { [@model_vc] !x > !x at L + !x at M }
variant { !x }
x := !x - 1
done
diff --git a/bench/ce/simple_array.mlw b/bench/ce/simple_array.mlw
index a86279dc62ca0ddd8631599af635eee0b87d1903..ab2c81760230840b4e91ca98333a98aeb3f39f95 100644
--- a/bench/ce/simple_array.mlw
+++ b/bench/ce/simple_array.mlw
@@ -2,7 +2,7 @@ theory ModelArray
use import map.Map
-goal t1 : forall t "model" :map int int, i "model" : int.
+goal t1 : forall t [@model] :map int int, i [@model] : int.
get (set t 0 42) i = get t i
end