Commit b6e01c68 authored by MARCHE Claude's avatar MARCHE Claude

Avoid polymorphism

parent 5a153a4e
......@@ -18,7 +18,13 @@ val add (x y : byte) : byte
requires { [@expl:integer overflow] in_range (to_int x + to_int y) }
ensures { to_int result = to_int x + to_int y }
end
module AbstractWithRef
use int.Int
use ref.Ref
use Abstract
let p3 (a : ref byte) =
a := add !a (of_int 1)
......
Strongest Postcondition
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout or Unknown
bench/ce/jlamp_projections.mlw AbstractWithRef VC p3: Valid
bench/ce/jlamp_projections.mlw AbstractWithRef VC p3: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 23:
Line 29:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
Line 24:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
......@@ -14,13 +14,13 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 35:
Line 41:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 36:
Line 42:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
......
Weakest Precondition
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout or Unknown
bench/ce/jlamp_projections.mlw AbstractWithRef VC p3: Valid
bench/ce/jlamp_projections.mlw AbstractWithRef VC p3: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 23:
Line 29:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
Line 24:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
......@@ -14,13 +14,13 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 35:
Line 41:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 36:
Line 42:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
......
Strongest Postcondition
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout or Unknown
bench/ce/jlamp_projections.mlw AbstractWithRef VC p3: Valid
bench/ce/jlamp_projections.mlw AbstractWithRef VC p3: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 23:
Line 29:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
Line 24:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (sat)
Counter-example model:File jlamp_projections.mlw:
Line 35:
Line 41:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 36:
Line 42:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
......
Weakest Precondition
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout or Unknown
bench/ce/jlamp_projections.mlw AbstractWithRef VC p3: Valid
bench/ce/jlamp_projections.mlw AbstractWithRef VC p3: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 23:
Line 29:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
Line 24:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (sat)
Counter-example model:File jlamp_projections.mlw:
Line 35:
Line 41:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 36:
Line 42:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "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