Commit 9c4127a8 authored by MARCHE Claude's avatar MARCHE Claude

CE bench: upgrade to new Why3 syntax

parent 5d5d9771
......@@ -19,7 +19,7 @@ run_cvc4_15 () {
../bin/why3prove.opt -P "CVC4,1.5" --timelimit 1 --get-ce $1 | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' > $1.out
sed 's/ ([0-9]\+\.[0-9]\+s)/ (time hidden)/' > $1.out
if cmp $1.oracle $1.out > /dev/null 2>&1 ; then
echo "ok"
else
......
......@@ -7,9 +7,9 @@ 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:x23" : ref int ): unit
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#*)
......@@ -20,9 +20,11 @@ module M
let test_loop ( x "model" "model_trace:x" : ref int ): unit
ensures { "model_vc_post" !x < old !x }
=
'L: incr x;
'M: while !x > 0 do
invariant { "model_vc" !x > at !x 'L + at !x 'M }
label L in
incr x;
label M in
while !x > 0 do
invariant { "model_vc" !x > !x at L + !x at M }
variant { !x }
x := !x - 1
done
......
......@@ -19,9 +19,9 @@ module M
function projf_r_g "model_trace:.g" (x : r) : bool
=
x.g
meta "inline : no" function projf_r_f
meta "inline:no" function projf_r_f
meta "model_projection" function projf_r_f
meta "inline : no" function projf_r_g
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
......
......@@ -28,9 +28,11 @@ module M
let test_loop ( x "model" "model_trace:x" : ref int ): unit
ensures { "model_vc_post" !x < old !x }
=
'L: incr x;
'M: while !x > 0 do
invariant { "model_vc" !x > at !x 'L + at !x 'M }
label L in
incr x;
label M in
while !x > 0 do
invariant { "model_vc" !x > !x at L + !x at M }
variant { !x }
x := !x - 1
done
......
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