Skip to content

GitLab

why3
why3
Commit 17bb76a2 authored by Benedikt Becker's avatar Benedikt Becker
Browse files
Options

Add bench/ce/loop_ce

parent 27f9a8f1
Hide whitespace changes
Inline Side-by-side
Showing with 316 additions and 0 deletions
bench/ce/loop_ce.mlw 0 → 100644
View file @ 17bb76a2
module M1
use int.Int
let ref a = 0
let ref b = 0
let f () =
a <- -1;
a <- 1;
b <- 2;
while b < 10 do
variant { 10 - b }
invariant { b - a < 5 }
b <- b + a;
done
end
module M2
use int.Int
let g (ref a: int) ensures { a = old a + 1 } =
label X in
if a <> 10 then a <- a + 1;
assert { a = a at X }
end
\ No newline at end of file
bench/ce/oracles/loop_ce_CVC4,1.7_SP.oracle 0 → 100644
View file @ 17bb76a2
Strongest Postcondition
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 8:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
Line 9:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 10:
b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 11:
[previous iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
Line 13:
[current iteration] a, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:b]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
Line 14:
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 23:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
a at X, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X], [@model_trace:a], [@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
old a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
bench/ce/oracles/loop_ce_CVC4,1.7_WP.oracle 0 → 100644
View file @ 17bb76a2
Weakest Precondition
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 9:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 10:
b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 11:
[previous iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
Line 13:
[current iteration] a, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:b]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
Line 14:
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 23:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
a at X, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X], [@model_trace:a], [@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Valid
bench/ce/loop_ce.mlw M2 g'vc: Valid
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
old a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
bench/ce/oracles/loop_ce_Z3,4.8.4_SP.oracle 0 → 100644
View file @ 17bb76a2
Strongest Postcondition
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 8:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
Line 9:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 10:
b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 11:
[previous iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
Line 13:
[current iteration] a, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:b]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
Line 14:
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 23:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
a at X, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X], [@model_trace:a], [@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
old a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
bench/ce/oracles/loop_ce_Z3,4.8.4_WP.oracle 0 → 100644
View file @ 17bb76a2
Weakest Precondition
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 9:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 10:
b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 11:
[previous iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
Line 13:
[current iteration] a, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:b]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
Line 14:
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 23:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
a at X, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X], [@model_trace:a], [@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Valid
bench/ce/loop_ce.mlw M2 g'vc: Valid
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
old a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
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