Commit 3f947d7e authored by Sylvain Dailler's avatar Sylvain Dailler

Adapting existing CE tests to ce-bench. Removed timings.

parent 3f4947b3
......@@ -15,7 +15,10 @@ esac
run_cvc4_15 () {
echo -n " $1... "
$dir/../bin/why3prove.opt -P "CVC4,1.5-prerelease" --get-ce $1 > $1.out
$dir/../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
if cmp $1.oracle $1.out > /dev/null 2>&1 ; then
echo "ok"
else
......
theory ModelInt
use import int.Int
(* PASS *)
goal test0 : forall x "model":int. not (0 < x < 1)
(* CE *)
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
(* CE *)
goal test_overflow:
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.
-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.
is_int16 x /\ is_int16 y -> is_int16 (x + y)
(* CE *)
goal test_overflow_int16_alt:
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.
is_int16 x /\ is_int16 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.
is_int32 x /\ is_int32 y -> is_int32 (x + y)
(* CE *)
goal test_overflow_int32_bis:
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.
-2147483648 <= x <= 2147483647 /\ -2147483648 <= y <= 2147483647 /\ 0 <= x <= y -> -2147483648 <= x + y <= 2147483647
end
./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
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)
if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
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:
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:
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:
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:
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:
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:
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:
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:
Line 58:
x = {"type" : "Integer" , "val" : "1073741824" }
y = {"type" : "Integer" ,
"val" : "1073741824" }
bench/ce/logic.mlw T g0 : Invalid (0.00s)
Counter-example model:File bench/ce/logic.mlw:
./ce/logic.mlw T g0 : Invalid
Counter-example model:File ./ce/logic.mlw:
Line 6:
x = {"type" : "Integer" ,
"val" : "48" }
bench/ce/logic.mlw T g1 : Invalid (0.00s)
Counter-example model:File bench/ce/logic.mlw:
./ce/logic.mlw T g1 : Invalid
Counter-example model:File ./ce/logic.mlw:
Line 10:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/logic.mlw T g2 : Invalid (0.00s)
Counter-example model:File bench/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" ,
......
module M
use import ref.Ref
use import list.List
use import int.Int
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
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 }
=
(*#"/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 }
=
'L: incr x;
'M: while !x > 0 do
invariant { "model_vc" !x > at !x 'L + at !x 'M }
variant { !x }
x := !x - 1
done
end
./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:
x23 = {"type" : "Integer" , "val" : "0" }
Line 13:
x23 = {"type" : "Integer" , "val" : "2" }
old x23 = {"type" : "Integer" ,
"val" : "0" }
y = {"type" : "Integer" ,
"val" : "0" }
Line 16:
y = {"type" : "Integer" , "val" : "0" }
Line 17:
x23 = {"type" : "Integer" , "val" : "1" }
Line 18:
x23 = {"type" : "Integer" ,
"val" : "2" }
./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:
x = {"type" : "Integer" , "val" : "0" }
old x = {"type" : "Integer" ,
"val" : "0" }
Line 23:
x = {"type" : "Integer" , "val" : "0" }
y = {"type" : "Integer" ,
"val" : "0" }
Line 24:
x = {"type" : "Integer" , "val" : "0" }
Line 25:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" ,
"val" : "0" }
theory ModelReal
use import real.Real
goal test1 : forall x "model":real. not (0.0 < x < 1.0)
goal test2 : forall x "model":real. x/x=1.0
end
./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)
if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
The fact in question: (= termITE_1 (/ x x))
")
module M
use import ref.Ref
use import list.List
use import int.Int
(*****************************************
** Getting counterexamples for records **
*****************************************)
(*** In all cases, records are decomposed using match eval ***)
type r = {f "model_trace:.field_f" :int; g:bool}
(* Projection functions *)
function projf_r_f "model_trace:.f" (x : r) : int
=
x.f
function projf_r_g "model_trace:.g" (x : r) : bool
=
x.g
meta "inline : no" function projf_r_f
meta "model_projection" function projf_r_f
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 }
=
if x.g then
x.f
else
1
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
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 }
=
x := { !x with f = 6 };
!x
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 }
=
x := { !x with f = 6 };
!x
end
./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" ,
"val" : false }
Line 28:
old x.g = {"type" : "Boolean" ,
"val" : false }
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:
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:
Line 40:
x.g = {"type" : "Boolean" ,
"val" : false }
Line 43:
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:
Line 45:
x.g = {"type" : "Boolean" ,
"val" : false }
Line 48:
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:
Line 51:
re.field_f = {"type" : "Integer" , "val" : "0" }
re.g = {"type" : "Boolean" ,
"val" : false }
Line 53:
x.g = {"type" : "Boolean" ,
"val" : false }
Line 56:
x.field_f = {"type" : "Integer" , "val" : "6" }
x.g = {"type" : "Boolean" ,
"val" : false }
File /home/sdailler/Projet/why3/share/modules/ref.mlw:
Line 18:
old re.field_f = {"type" : "Integer" ,
"val" : "0" }
old re.g = {"type" : "Boolean" ,
"val" : false }
x.field_f = {"type" : "Integer" ,
"val" : "6" }
x.g = {"type" : "Boolean" ,
"val" : false }
module M
use import ref.Ref
use import list.List
use import int.Int
type int_type = Integer int
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 }
=
y := x - 1 + !y
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
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 }
=
(*#"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 }
=
'L: incr x;
'M: while !x > 0 do
invariant { "model_vc" !x > at !x 'L + at !x 'M }
variant { !x }
x := !x - 1
done
end
./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" ,
"val" : "0" }
Line 11:
old x = {"type" : "Integer" , "val" : "0" }
old y = {"type" : "Integer" ,
"val" : "0" }
Line 13:
y = {"type" : "Integer" ,
"val" : "0" }
./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:
x23 = {"type" : "Integer" , "val" : "0" }
Line 21:
x23 = {"type" : "Integer" , "val" : "2" }
old x23 = {"type" : "Integer" ,
"val" : "0" }
y = {"type" : "Integer" ,
"val" : "0" }
Line 24:
y = {"type" : "Integer" , "val" : "0" }
Line 25:
x23 = {"type" : "Integer" , "val" : "1" }
Line 26:
x23 = {"type" : "Integer" ,
"val" : "2" }
./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:
x = {"type" : "Integer" , "val" : "0" }
old x = {"type" : "Integer" ,
"val" : "0" }
Line 31:
x = {"type" : "Integer" , "val" : "0" }
y = {"type" : "Integer" ,
"val" : "0" }
Line 32:
x = {"type" : "Integer" , "val" : "0" }
Line 33:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" ,
"val" : "0" }
theory ModelArray
use import map.Map
goal t1 : forall t "model" :map int int, i "model" : int.
get (set t 0 42) i = get t i
end
./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" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "43" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
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