Commit ca07a3cc authored by MARCHE Claude's avatar MARCHE Claude

CE examples: removing useless labels

parent 31094ffb
......@@ -15,22 +15,22 @@ module Array
axiom three_def : to_int three = 3
let f (a :array t) : unit
let f (a : array t) : unit
requires { a[42] = three }
writes { a }
ensures { a[42] = three }
= a[42] <- two
let g (a "model" "model_projected" :array t) : unit
let g (a : array t) : unit
requires { a.length >= 43 /\ a[17] = three }
writes { a }
ensures { "model_vc" a[42] = three }
ensures { a[42] = three }
= a[42] <- two
let h (a "model" "model_projected" :array t) : unit
let h (a : array t) : unit
requires { a.length >= 43 /\ a[17] = three }
writes { a }
ensures { "model_vc" a[42] = three }
ensures { a[42] = three }
= a[17] <- two
end
......@@ -20,7 +20,7 @@ val add (x y : byte) : byte
use import ref.Ref
let p3 (a "model_projected" : ref byte) =
let p3 (a : ref byte) =
a := add !a (of_int 1)
end
......@@ -31,12 +31,7 @@ use import int.Int
use import Abstract
type r = {mutable f : byte; mutable g : bool}
(*
function get_f (x:r) : byte = x.f
function get_g (x:r) : bool = x.g
meta model_projection function get_f
meta model_projection function get_g
*)
let p4 (b : r) =
if b.g then b.f <- add b.f (of_int 1)
......
......@@ -10,11 +10,11 @@ a = {"type" : "Integer" ,
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
Counter-example model:File jlamp_projections.mlw:
Line 40:
Line 35:
b.f = {"type" : "Integer" , "val" : "127" }
b.g = {"type" : "Boolean" ,
"val" : true }
Line 41:
Line 36:
b.f = {"type" : "Integer" ,
"val" : "127" }
......@@ -30,11 +30,11 @@ a = {"type" : "Integer" ,
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
Counter-example model:File jlamp_projections.mlw:
Line 40:
Line 35:
b.f = {"type" : "Integer" , "val" : "127" }
b.g = {"type" : "Boolean" ,
"val" : true }
Line 41:
Line 36:
b.f = {"type" : "Integer" ,
"val" : "127" }
......@@ -3,10 +3,10 @@ bench/ce/jlamp_projections.mlw Abstract WP_parameter p3 : Unknown (other)
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
Counter-example model:File jlamp_projections.mlw:
Line 40:
Line 35:
b.g = {"type" : "Boolean" ,
"val" : true }
Line 41:
Line 36:
the check fails with all inputs
bench/ce/jlamp_projections.mlw Abstract WP_parameter p3 : Valid
......@@ -14,9 +14,9 @@ bench/ce/jlamp_projections.mlw Abstract WP_parameter p3 : Unknown (other)
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
Counter-example model:File jlamp_projections.mlw:
Line 40:
Line 35:
b.g = {"type" : "Boolean" ,
"val" : true }
Line 41:
Line 36:
the check fails with all inputs
......@@ -3,10 +3,10 @@ bench/ce/jlamp_projections.mlw Abstract WP_parameter p3 : Unknown (other)
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
Counter-example model:File jlamp_projections.mlw:
Line 40:
Line 35:
b.g = {"type" : "Boolean" ,
"val" : true }
Line 41:
Line 36:
the check fails with all inputs
bench/ce/jlamp_projections.mlw Abstract WP_parameter p3 : Valid
......@@ -14,9 +14,9 @@ bench/ce/jlamp_projections.mlw Abstract WP_parameter p3 : Unknown (other)
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
bench/ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
Counter-example model:File jlamp_projections.mlw:
Line 40:
Line 35:
b.g = {"type" : "Boolean" ,
"val" : true }
Line 41:
Line 36:
the check fails with all inputs
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