Commit 1218b433 authored by Sylvain Dailler's avatar Sylvain Dailler

ce-bench: Add test with two projection for the same type

parent ffd771b9
module Test
use int.Int
type t
function d (x : t) : int
meta "model_projection" function d
function c (x : t) : int
meta "model_projection" function c
(* Here the counterexample should not be a record *)
let f (x: t) : t
requires { c x > 0 }
ensures { d x < 0 }
=
x
end
Strongest Postcondition
bench/ce/double_projection.mlw Test VC f: Timeout or Unknown
Counter-example model:File double_projection.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 19:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Weakest Precondition
bench/ce/double_projection.mlw Test VC f: Timeout or Unknown
Counter-example model:File double_projection.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 19:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Strongest Postcondition
bench/ce/double_projection.mlw Test VC f: Unknown (sat)
Counter-example model:File double_projection.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 19:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Weakest Precondition
bench/ce/double_projection.mlw Test VC f: Unknown (sat)
Counter-example model:File double_projection.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 19:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "d" , "value" : {"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