Commit bff0a1f9 authored by MARCHE Claude's avatar MARCHE Claude

CE bench: enforce execution with cwd = the directory bench/

otherwise, superfluous diff may show up
parent 3f947d7e
......@@ -12,13 +12,14 @@ case "$1" in
exit 2
esac
cd $dir
run_cvc4_15 () {
echo -n " $1... "
$dir/../bin/why3prove.opt -P "CVC4,1.5-prerelease" --timelimit 5 --get-ce $1 | \
../bin/why3prove.opt -P "CVC4,1.5-prerelease" --timelimit 5 --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)//' > $1.out
if cmp $1.oracle $1.out > /dev/null 2>&1 ; then
echo "ok"
else
......@@ -37,6 +38,6 @@ run_cvc4_15 () {
for f in $dir/ce/*.mlw; do
for f in ce/*.mlw; do
run_cvc4_15 $f
done
./ce/int_overflow.mlw ModelInt test0 : Valid
./ce/int_overflow.mlw ModelInt test1 : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
./ce/int_overflow.mlw ModelInt test2 : HighFailure
ce/int_overflow.mlw ModelInt test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
(error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (INTS_DIVISION_TOTAL x x)
......@@ -14,57 +14,57 @@ The fact in question: (= termITE_1 (INTS_DIVISION_TOTAL x x))
")
./ce/int_overflow.mlw ModelInt test_overflow : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test_overflow : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 18:
x = {"type" : "Integer" , "val" : "65535" }
y = {"type" : "Integer" ,
"val" : "1" }
./ce/int_overflow.mlw ModelInt test_overflow2 : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test_overflow2 : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 23:
x = {"type" : "Integer" , "val" : "-2" }
y = {"type" : "Integer" ,
"val" : "-1" }
./ce/int_overflow.mlw ModelInt test_overflow_int16 : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test_overflow_int16 : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 30:
x = {"type" : "Integer" , "val" : "-65536" }
y = {"type" : "Integer" ,
"val" : "-1" }
./ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 35:
x = {"type" : "Integer" , "val" : "-65536" }
y = {"type" : "Integer" ,
"val" : "-1" }
./ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 40:
x = {"type" : "Integer" , "val" : "32768" }
y = {"type" : "Integer" ,
"val" : "32768" }
./ce/int_overflow.mlw ModelInt test_overflow_int32 : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test_overflow_int32 : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 48:
x = {"type" : "Integer" , "val" : "-2147483648" }
y = {"type" : "Integer" ,
"val" : "-1" }
./ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 53:
x = {"type" : "Integer" , "val" : "1073741824" }
y = {"type" : "Integer" ,
"val" : "1073741824" }
./ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Invalid
Counter-example model:File ./ce/int_overflow.mlw:
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Invalid
Counter-example model:File ce/int_overflow.mlw:
Line 58:
x = {"type" : "Integer" , "val" : "1073741824" }
y = {"type" : "Integer" ,
......
./ce/logic.mlw T g0 : Invalid
Counter-example model:File ./ce/logic.mlw:
ce/logic.mlw T g0 : Invalid
Counter-example model:File ce/logic.mlw:
Line 6:
x = {"type" : "Integer" ,
"val" : "48" }
./ce/logic.mlw T g1 : Invalid
Counter-example model:File ./ce/logic.mlw:
ce/logic.mlw T g1 : Invalid
Counter-example model:File ce/logic.mlw:
Line 10:
x = {"type" : "Integer" ,
"val" : "0" }
./ce/logic.mlw T g2 : Invalid
Counter-example model:File ./ce/logic.mlw:
ce/logic.mlw T g2 : Invalid
Counter-example model:File ce/logic.mlw:
Line 12:
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
......
./ce/map.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File ./ce/map.mlw:
ce/map.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File ce/map.mlw:
Line 10:
y = {"type" : "Integer" , "val" : "-1" }
Line 12:
......@@ -18,8 +18,8 @@ Line 18:
x23 = {"type" : "Integer" ,
"val" : "2" }
./ce/map.mlw M WP_parameter test_loop : Unknown (other)
Counter-example model:File ./ce/map.mlw:
ce/map.mlw M WP_parameter test_loop : Unknown (other)
Counter-example model:File ce/map.mlw:
Line 20:
x = {"type" : "Integer" , "val" : "0" }
Line 21:
......
./ce/real.mlw ModelReal test1 : Invalid
./ce/real.mlw ModelReal test2 : HighFailure
ce/real.mlw ModelReal test1 : Invalid
ce/real.mlw ModelReal test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
(error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ x x)
......
./ce/records.mlw M WP_parameter record_match_eval_test1 : Unknown (other)
Counter-example model:File ./ce/records.mlw:
ce/records.mlw M WP_parameter record_match_eval_test1 : Unknown (other)
Counter-example model:File ce/records.mlw:
Line 27:
x.field_f = {"type" : "Integer" , "val" : "0" }
x.g = {"type" : "Boolean" ,
......@@ -10,14 +10,14 @@ old x.g = {"type" : "Boolean" ,
old x.field_f = {"type" : "Integer" ,
"val" : "0" }
./ce/records.mlw M WP_parameter record_match_eval_test2 : Unknown (other)
Counter-example model:File ./ce/records.mlw:
ce/records.mlw M WP_parameter record_match_eval_test2 : Unknown (other)
Counter-example model:File ce/records.mlw:
Line 35:
x.field_f = {"type" : "Integer" ,
"val" : "0" }
./ce/records.mlw M WP_parameter record_match_eval_test3 : Unknown (other)
Counter-example model:File ./ce/records.mlw:
ce/records.mlw M WP_parameter record_match_eval_test3 : Unknown (other)
Counter-example model:File ce/records.mlw:
Line 40:
x.g = {"type" : "Boolean" ,
"val" : false }
......@@ -26,8 +26,8 @@ x.field_f = {"type" : "Integer" , "val" : "6" }
x.g = {"type" : "Boolean" ,
"val" : false }
./ce/records.mlw M WP_parameter record_match_eval_test4 : Unknown (other)
Counter-example model:File ./ce/records.mlw:
ce/records.mlw M WP_parameter record_match_eval_test4 : Unknown (other)
Counter-example model:File ce/records.mlw:
Line 45:
x.g = {"type" : "Boolean" ,
"val" : false }
......@@ -36,8 +36,8 @@ x.field_f = {"type" : "Integer" , "val" : "6" }
x.g = {"type" : "Boolean" ,
"val" : false }
./ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other)
Counter-example model:File ./ce/records.mlw:
ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other)
Counter-example model:File ce/records.mlw:
Line 51:
re.field_f = {"type" : "Integer" , "val" : "0" }
re.g = {"type" : "Boolean" ,
......
./ce/ref.mlw M G : Unknown (other)
./ce/ref.mlw M WP_parameter test_post : Unknown (other)
Counter-example model:File ./ce/ref.mlw:
ce/ref.mlw M G : Unknown (other)
ce/ref.mlw M WP_parameter test_post : Unknown (other)
Counter-example model:File ce/ref.mlw:
Line 10:
x = {"type" : "Integer" , "val" : "0" }
y = {"type" : "Integer" ,
......@@ -13,8 +13,8 @@ Line 13:
y = {"type" : "Integer" ,
"val" : "0" }
./ce/ref.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File ./ce/ref.mlw:
ce/ref.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File ce/ref.mlw:
Line 18:
y = {"type" : "Integer" , "val" : "-1" }
Line 20:
......@@ -33,8 +33,8 @@ Line 26:
x23 = {"type" : "Integer" ,
"val" : "2" }
./ce/ref.mlw M WP_parameter test_loop : Unknown (other)
Counter-example model:File ./ce/ref.mlw:
ce/ref.mlw M WP_parameter test_loop : Unknown (other)
Counter-example model:File ce/ref.mlw:
Line 28:
x = {"type" : "Integer" , "val" : "0" }
Line 29:
......
./ce/simple_array.mlw ModelArray t1 : Invalid
Counter-example model:File ./ce/simple_array.mlw:
ce/simple_array.mlw ModelArray t1 : Invalid
Counter-example model:File ce/simple_array.mlw:
Line 5:
i = {"type" : "Integer" , "val" : "0" }
t = {"type" : "Array" ,
......
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