Commit 0f7e207c authored by Sylvain Dailler's avatar Sylvain Dailler

Update ce-bench and order printed file

parent bff0a1f9
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Invalid
Counter-example model:File ce/int_overflow.mlw:
Counter-example model:File int_overflow.mlw:
Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
......@@ -8,63 +8,62 @@ x = {"type" : "Integer" ,
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))
(error "A non-linear fact was asserted to arithmetic in a linear logic.
The fact in question: (>= (+ x (* (- 1) (* x linearIntDiv_1))) 0)
")
ce/int_overflow.mlw ModelInt test_overflow : Invalid
Counter-example model:File ce/int_overflow.mlw:
Counter-example model:File 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:
Counter-example model:File 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:
Counter-example model:File 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:
Counter-example model:File 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:
Counter-example model:File 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:
Counter-example model:File 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:
Counter-example model:File 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:
Counter-example model:File 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:
Counter-example model:File logic.mlw:
Line 6:
x = {"type" : "Integer" ,
"val" : "48" }
ce/logic.mlw T g1 : Invalid
Counter-example model:File ce/logic.mlw:
Counter-example model:File logic.mlw:
Line 10:
x = {"type" : "Integer" ,
"val" : "0" }
ce/logic.mlw T g2 : Invalid
Counter-example model:File ce/logic.mlw:
Counter-example model:File 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:
Counter-example model:File map.mlw:
Line 10:
y = {"type" : "Integer" , "val" : "-1" }
Line 12:
......@@ -19,7 +19,7 @@ x23 = {"type" : "Integer" ,
"val" : "2" }
ce/map.mlw M WP_parameter test_loop : Unknown (other)
Counter-example model:File ce/map.mlw:
Counter-example model:File map.mlw:
Line 20:
x = {"type" : "Integer" , "val" : "0" }
Line 21:
......
......@@ -2,9 +2,8 @@ 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))
(error "A non-linear fact was asserted to arithmetic in a linear logic.
The fact in question: (= x (* x nonlinearDiv_1))
")
ce/records.mlw M WP_parameter record_match_eval_test1 : Unknown (other)
Counter-example model:File ce/records.mlw:
Counter-example model:File records.mlw:
Line 27:
x.field_f = {"type" : "Integer" , "val" : "0" }
x.g = {"type" : "Boolean" ,
......@@ -11,13 +11,13 @@ 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:
Counter-example model:File 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:
Counter-example model:File records.mlw:
Line 40:
x.g = {"type" : "Boolean" ,
"val" : false }
......@@ -27,7 +27,7 @@ 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:
Counter-example model:File records.mlw:
Line 45:
x.g = {"type" : "Boolean" ,
"val" : false }
......@@ -37,7 +37,17 @@ 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:
Counter-example model:File 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 }
File records.mlw:
Line 51:
re.field_f = {"type" : "Integer" , "val" : "0" }
re.g = {"type" : "Boolean" ,
......@@ -49,14 +59,4 @@ 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 }
ce/ref.mlw M G : Unknown (other)
ce/ref.mlw M WP_parameter test_post : Unknown (other)
Counter-example model:File ce/ref.mlw:
Counter-example model:File ref.mlw:
Line 10:
x = {"type" : "Integer" , "val" : "0" }
y = {"type" : "Integer" ,
......@@ -14,7 +14,7 @@ y = {"type" : "Integer" ,
"val" : "0" }
ce/ref.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File ce/ref.mlw:
Counter-example model:File ref.mlw:
Line 18:
y = {"type" : "Integer" , "val" : "-1" }
Line 20:
......@@ -34,7 +34,7 @@ x23 = {"type" : "Integer" ,
"val" : "2" }
ce/ref.mlw M WP_parameter test_loop : Unknown (other)
Counter-example model:File ce/ref.mlw:
Counter-example model:File 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:
Counter-example model:File simple_array.mlw:
Line 5:
i = {"type" : "Integer" , "val" : "0" }
t = {"type" : "Array" ,
......
......@@ -278,6 +278,10 @@ let print_model_elements ?(sep = "\n") me_name_trans fmt m_elements =
Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element me_name_trans) fmt m_elements
let print_model_file fmt me_name_trans filename model_file =
(* Relativize does not work on nighly bench: using path_of_file instead. It
hides the local paths. *)
let path = Sysutil.path_of_file filename in
let filename = List.hd (List.rev path) in
fprintf fmt "File %s:" filename;
IntMap.iter
(fun line m_elements ->
......@@ -296,7 +300,9 @@ let print_model
?(me_name_trans = why_name_trans)
fmt
model =
StringMap.iter (print_model_file fmt me_name_trans) model.model_files
(* Simple and easy way to print file sorted alphabetically *)
let l = StringMap.bindings model.model_files in
List.iter (fun (k, e) -> print_model_file fmt me_name_trans k e) l
let model_to_string
?(me_name_trans = why_name_trans)
......
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