Check syntax of bench/ce files.

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

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

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

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

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

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

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

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