Commit 0a69b161 authored by Sylvain Dailler's avatar Sylvain Dailler

Merge branch 'rebase_collecting_counterex'

Merge typing.ml and remove ref that is now apparently a keyword.
parents 10e54f43 37c89aad
......@@ -39,7 +39,12 @@ run () {
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' >> "$f.out"
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' | \
# ad hoc sed to remove the directory of the stdlib that can be found
# inside labels attribute [@at:'Old:loc:/home/.../stdlib/array.mlw
# TODO temporary as this comes from incorrect locations generated in
# a[i] <- x like terms.
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' >> "$f.out"
printf "SP $2 ($1)... "
echo "Strongest Postcondition" >> "$f.out"
$dir/../bin/why3prove.opt --debug print_model_attrs --debug vc_sp -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
......@@ -48,7 +53,12 @@ run () {
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' >> "$f.out"
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' | \
# ad hoc sed to remove the directory of the stdlib that can be found
# inside labels attribute [@at:'Old:loc:/home/.../stdlib/array.mlw
# TODO temporary as this comes from incorrect locations generated in
# a[i] <- x like terms.
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' >> "$f.out"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
else
......
......@@ -26,11 +26,11 @@ module M
goal g7: forall l: mylist. l = Nil
(* use list.List
use list.List
use list.Length
goal g: forall l: list int. length l = 0
*)
(*
(*********************************
......
......@@ -14,6 +14,12 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 16:
......@@ -23,7 +29,22 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "1" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "-1" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "0" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
......@@ -40,6 +61,12 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 16:
......@@ -49,4 +76,19 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "1" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "-1" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "0" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
......@@ -14,6 +14,12 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
......@@ -23,7 +29,34 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "21" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "10" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "9" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "7" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "8" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
......@@ -40,6 +73,12 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
......@@ -49,4 +88,31 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "21" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "10" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "9" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "7" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "8" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
module Array
use int.Int
use map.Map
type array = private {
mutable ghost elts : int -> int;
length : int
} invariant { 0 <= length }
function ([]) (a: array) (i: int) : int = a.elts i
val ([]) (a: array) (i: int) : int
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { result = a[i] }
val ghost function ([<-]) (a: array) (i: int) (v: int): array
ensures { result.length = a.length }
ensures { result.elts = Map.set a.elts i v }
val ([]<-) (a: array) (i: int) (v: int) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { a.elts = Map.set (old a).elts i v }
ensures { a = (old a)[i <- v] }
end
module A
use int.Int
use Array
let f1 (a:array) : int
= a[0]
let f2 (a:array) : unit
requires { a.length >= 2 }
ensures { a[0] <> a[1] }
= a[0] <- 42
end
(*
module B
use int.Int
use array.Array
clone array.Sorted with
type elt=int,
predicate le=(<=)
let f1 (a:array int) : unit
ensures { sorted a }
= ()
let f2 (a:array int) : array int
ensures { sorted result }
= a
end
*)
\ No newline at end of file
Weakest Precondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 35:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 38:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Strongest Postcondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 35:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 38:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Weakest Precondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 35:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 38:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Strongest Postcondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 35:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 38:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
This diff is collapsed.
......@@ -4,17 +4,21 @@ 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], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "22" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Line 9:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "42" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Line 10:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
......@@ -22,9 +26,11 @@ 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], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "22" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
......@@ -4,17 +4,21 @@ 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], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "22" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Line 9:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "42" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Line 10:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
......@@ -22,9 +26,11 @@ 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], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "22" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
......@@ -2,146 +2,191 @@ Weakest Precondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 22:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 22:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 24:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,