Commit 6fe0fb76 authored by MARCHE Claude's avatar MARCHE Claude

CE: new example on bitvectors

parent 0c4709dc
module Ce_int32bv
use mach.bv.BVCheck32
type bv32 = BVCheck32.t
let dummy_update (ref r : bv32)
requires { r = (0x22:bv32) }
ensures { r = (0x42:bv32) } =
r <- (0x42:bv32);
r <- add r r
let dummy_update_with_int (ref r : bv32)
requires { t'int r = 0x22 }
ensures { t'int r = 0x42 } =
r <- (0x42:bv32);
r <- add r r
end
module Ce_int32
use ref.Ref
use export mach.int.Int32
use mach.int.Int32
let dummy_update (r: ref int32)
requires { int32'int !r = 22}
ensures { int32'int !r = 42} =
r := (42:int32);
r := !r + !r;
let dummy_update (ref r : int32)
requires { int32'int r = 22}
ensures { int32'int r = 42} =
r <- (42:int32);
r <- r + r;
end
Strongest Postcondition
bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
Counter-example model:File bv32.mlw:
Line 7:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "34" } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "132" } }] } }
Line 10:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "66" } }] } }
Line 11:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "132" } }] } }
bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
Counter-example model:File bv32.mlw:
Line 13:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "0" } }] } }
Line 15:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "0" } }] } }
Line 16:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "0" } }] } }
Line 17:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "4294967295" } }] } }
Weakest Precondition
bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
Counter-example model:File bv32.mlw:
Line 7:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "34" } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "132" } }] } }
Line 10:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "66" } }] } }
Line 11:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "132" } }] } }
bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
Counter-example model:File bv32.mlw:
Line 13:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "0" } }] } }
Line 15:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "0" } }] } }
Line 16:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "0" } }] } }
Line 17:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
"val" : "4294967295" } }] } }
Strongest Postcondition
bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
Weakest Precondition
bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
......@@ -2,27 +2,30 @@ Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 5:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 8:
r, [[@introduced], [@field:0:contents],
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
Line 9:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 8:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } } }] } }
Line 10:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 9:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -2,27 +2,30 @@ Weakest Precondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 5:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 8:
r, [[@introduced], [@field:0:contents],
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
Line 9:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 8:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } } }] } }
Line 10:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 9:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -2,27 +2,30 @@ Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 5:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 8:
r, [[@introduced], [@field:0:contents],
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
Line 9:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 8:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } } }] } }
Line 10:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 9:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -2,27 +2,30 @@ Weakest Precondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 5:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 8:
r, [[@introduced], [@field:0:contents],
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
Line 9:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 8:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } } }] } }
Line 10:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 9:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
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