Commit 374fe4df authored by MARCHE Claude's avatar MARCHE Claude

CE bench: remove useless labels

parent 0ca4f82b
......@@ -15,10 +15,10 @@ module Array
axiom three_def : to_int three = 3
let f (a "model" "model_projected" :array t) : unit
let f (a :array t) : unit
requires { a[42] = three }
writes { a }
ensures { "model_vc" a[42] = three }
ensures { a[42] = three }
= a[42] <- two
let g (a "model" "model_projected" :array t) : unit
......
......@@ -31,13 +31,13 @@ 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 "model_projected" : r) =
*)
let p4 (b : r) =
if b.g then b.f <- add b.f (of_int 1)
end
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