Skip to content
Commits on Source (4)
Show whitespace changes
Inline Side-by-side
.merlin.in
View file @ 43d39707
......@@ -41,4 +41,4 @@ B plugins/tptp
B plugins/python
B lib/why3
PKG str unix num dynlink @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@
PKG str unix num dynlink @ZIPLIB@ @LABLGTKPKG@ @META_OCAMLGRAPH@ @JSOFOCAMLPKG@
CHANGES.md
View file @ 43d39707
:x: marks a potential source of incompatibility
Version 1.2.0, February 11, 2019
--------------------------------
Session
* file path stored in session files are now represented in a
system-independent way
Drivers
* the clause `syntax converter` has been removed; any former use should
be replaced by `syntax literal` and/or `syntax function` :x:
Language
* the `any` expression is now always ghost :x:
* a syntactic sugar called "auto-dereference" is introduced, so as
to avoid, on simple programs, the heavy use of `(!)` character on
references; see details in Section A.1 of the manual
Transformations
* `split_vc` and `subst_all` now avoid substituting user symbols by
generated ones :x:
* `destruct_rec` applies `destruct` recursively on a goal
* `destruct` now simplifies away equalities on constructors :x:
* `destruct` now simplifies `if .. then .. else ..` and `match .. with ..` :x:
* `destruct_alg` renamed to `destruct_term`; it also has a new experimental
keyword `using` to name newly destructed elements :x:
Tools
* added a command `why3 session update` to modify sessions from the
command line; so far, only option `-rename-file` exists, for
renaming files
* `why3 config --add-prover` now takes the shortcut as second
argument; option `--list-prover-ids` has been renamed to
`--list-prover-families` :x:
IDE
* clicking on the status of a failed proof attempt in the proof tree
now generates counterexamples
* added support for GTK3
Counterexamples
* the trigger for counterexamples has been changed; read Section 5.3.7
of the manual for details :x:
* various improvements on the generated counterexamples
* field names now use ident names instead of smt generated ones, e.g.,
`int32qtint` -> `int32'int` :x:
* fixed parsing of bitvector values from counterexamples generated by Z3
Extraction
* fixed extraction of functions passed as arguments
* fixed extraction of recursive polymorphic functions for Ocaml
* improved extraction of records for C
Standard library
* `Stack.length` and `Queue.length` now return a `Peano.t`, for
improved extraction :x:
Provers
* support for Z3 4.8.1 (released Oct 16, 2018)
* support for Z3 4.8.3 (released Nov 20, 2018)
* support for Z3 4.8.4 (released Dec 20, 2018)
* support for Coq 8.9.0 (released Jan 17, 2019)
* upgraded Coq realizations for floating-point arithmetic to Flocq 3.1
Version 1.1.1, December 17, 2018
--------------------------------
......
Makefile.in
View file @ 43d39707
####################################################################
# #
# The Why3 Verification Platform / The Why3 Development Team #
# Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University #
# Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University #
# #
# This software is distributed under the terms of the GNU Lesser #
# General Public License version 2.1, with the special exception #
......@@ -218,11 +218,11 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \
encoding_sort simplify_array filter_trigger \
abstraction close_epsilon lift_epsilon \
eliminate_epsilon intro_projections_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
instantiate_predicate smoke_detector \
prop_curry eliminate_literal \
generic_arg_trans_utils case apply subst \
introduction ind_itp destruct cut \
introduction ind_itp destruct cut congruence \
intro_vc_vars_counterexmp prepare_for_counterexmp \
induction induction_pr matching reflection
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
......@@ -723,7 +723,9 @@ xml-validate-local:
ifeq (@enable_ide@,yes)
IDE_FILES = gconfig ide_utils why3ide
IDEGENERATED = src/ide/gtkcompat.ml
IDE_FILES = gtkcompat gconfig ide_utils why3ide
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -734,13 +736,15 @@ IDECMX = $(addsuffix .cmx, $(IDEMODULES))
$(IDEDEP): DEPFLAGS += -I src/ide
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
$(IDEDEP): $(IDEGENERATED)
# build targets
byte: bin/why3ide.byte
opt: bin/why3ide.opt
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.opt bin/why3ide.byte: INCLUDES += @LABLGTKINCLUDE@
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += @LABLGTKLIB@
bin/why3ide.byte: BLINKFLAGS += -custom
bin/why3ide.opt: $(WHY3CMXA) src/ide/resetgc.o $(IDECMX)
......@@ -784,8 +788,17 @@ install:: install-ide
install_local:: bin/why3ide
ifeq (@GTKVERSION@,2)
src/ide/gtkcompat.ml: config.status src/ide/gtkcompat2.ml
cp src/ide/gtkcompat2.ml $@
else
src/ide/gtkcompat.ml: config.status src/ide/gtkcompat3.ml
cp src/ide/gtkcompat3.ml $@
endif
GENERATED += $(IDEGENERATED)
endif
###############
# WEBSERV
......@@ -840,7 +853,7 @@ install_local:: bin/why3webserver
###############
SESSION_FILES = why3session_lib why3session_info \
why3session_html why3session_latex \
why3session_html why3session_latex why3session_update \
why3session_main
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
# why3session_output
......@@ -1850,6 +1863,21 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
test-ce.byte: examples/use_api/counterexample.ml lib/why3/why3.cma
$(SHOW) 'Ocaml $<'
$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
|| (rm -f why3session.xml why3shapes why3shapes.gz; \
printf "Test of Why3 API calls for counterexamples failed. Please fix it"; exit 2)
@rm -f why3session.xml why3shapes why3shapes.gz
test-ce.opt: examples/use_api/counterexample.ml lib/why3/why3.cmxa
$(SHOW) 'Ocamlopt $<'
$(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-ce.opt > /dev/null) \
|| (rm -f test-ce.opt why3session.xml why3shapes why3shapes.gz; \
printf "Test of Why3 API calls for counterexamples failed. Please fix it"; exit 2)
@rm -f test-ce.opt why3session.xml why3shapes why3shapes.gz
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat clean
......@@ -1911,6 +1939,10 @@ doc/generated/mlw_tree__%.ml: examples/use_api/mlw_tree.ml doc/extract_ocaml_cod
doc/generated/transform__%.ml: examples/use_api/transform.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@
doc/generated/counterexample__%.ml: examples/use_api/counterexample.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@
OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \
buildtask printtask buildtask2 \
getconf getanyaltergo getaltergo200 \
......@@ -1928,11 +1960,15 @@ OCAMLCODE_MLWTREE = buildenv openmodule useimport \
source1 code1 helper1 source2 code2 source3 code3 \
closemodule checkingvcs
OCAMLCODE_COUNTEREXAMPLES = ce_declarepropvars ce_adaptgoals \
ce_get_cvc4ce ce_callprover ce_nobuiltin
OCAMLCODE = \
$(addprefix doc/generated/logic__, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \
$(addprefix doc/generated/call_provers__, $(addsuffix .ml, $(OCAMLCODE_CALLPROVERS))) \
$(addprefix doc/generated/transform__, $(addsuffix .ml, $(OCAMLCODE_TRANSFORM))) \
$(addprefix doc/generated/mlw_tree__, $(addsuffix .ml, $(OCAMLCODE_MLWTREE))) \
$(addprefix doc/generated/counterexample__, $(addsuffix .ml, $(OCAMLCODE_COUNTEREXAMPLES))) \
doc/generated/whyconf__provertype.ml
DOC = api glossary ide intro exec macros manpages install \
......@@ -2060,6 +2096,8 @@ install:: install-bash
STDLIBS = \
algebra \
appmap \
appset \
array \
bag \
bintree \
......@@ -2069,6 +2107,7 @@ STDLIBS = \
graph \
hashtbl \
ieee_float \
impmap \
impset \
int \
list \
......
Version
View file @ 43d39707
VERSION=1.1.1
VERSION=1.2.0
bench/bench
View file @ 43d39707
......@@ -159,6 +159,26 @@ execute () {
fi
}
extract () {
pgm="bin/why3extract$suffix"
dir=$1
shift
for f in $dir/*.mlw; do
printf " $f... "
if ($pgm $@ $f -o bench_test.ml && ocaml -noinit bench_test.ml) > /dev/null 2> /dev/null; then
echo "ok"
else
echo "extract test failed!"
echo $pgm $@ $f
$pgm $@ $f -o bench_test.ml
ocaml -noinit bench_test.ml
rm -f bench_test.ml
exit 1
fi
done
rm -f bench_test.ml
}
extract_and_run () {
dir=$1
shift
......@@ -349,6 +369,7 @@ execute examples/vstte10_queens.mlw NQueens.test8
echo ""
echo "=== Checking extraction to OCaml ==="
extract bench/extraction -D ocaml64
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
......
bench/ce-bench
View file @ 43d39707
......@@ -26,50 +26,102 @@ if test "$files" = "" ; then
files="$dir/ce/*.mlw"
fi
is_xfail=none
# $1 = prover, $2 = file
# TODO this function should disappear as counterexamples should eventually get
# more reproducible.
decide_fail () {
case "$1" in
# Inconsistent integer values between two runs
"bench/ce/algebraic_types_mono_Z3,4.6.0_SP")
is_xfail=integer_values;;
# Inconsistent results between two runs
"bench/ce/algebraic_types_mono_Z3,4.6.0_WP")
is_xfail=integer_values;;
# Inconsistent results between two runs
"bench/ce/ref_mono_Z3,4.6.0_WP")
is_xfail=integer_values;;
# Inconsistent results between two runs
"bench/ce/ref_mono_Z3,4.6.0_SP")
is_xfail=integer_values;;
*) is_xfail=none;;
esac
}
# $1 = prover, $2 = dir, $3 = filename, $4 = true for WP; false for SP
run () {
printf " $2 ($1)... "
f="$2_$1"
printf "WP $2 ($1)... "
file_path="$2/$3"
if $4; then
f="${file_path}_$1_WP"
oracle_file="$2/oracles/$3_$1_WP.oracle"
wp_sp=""
echo "Weakest Precondition" > "$f.out"
$dir/../bin/why3prove.opt --debug print_attrs -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
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"
printf "SP $2 ($1)... "
echo "Strongest Postcondition" >> "$f.out"
$dir/../bin/why3prove.opt --debug print_attrs --debug vc_sp -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
printf "Weakest Precondition ${file_path} ($1)... "
else
f="${file_path}_$1_SP"
oracle_file="$2/oracles/$3_$1_SP.oracle"
wp_sp=" --debug vc_sp"
echo "Strongest Postcondition" > "$f.out"
printf "Strongest Postcondition ${file_path} ($1)... "
fi
$dir/../bin/why3prove.opt --debug print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit 1 -a split_vc "${file_path}.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
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"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
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"
str_oracle=$(tr -d ' \n' < "${oracle_file}")
str_out=$(tr -d ' \n' < "$f.out")
decide_fail $f
case $is_xfail in
"full") is_xfail=true;;
"none") is_xfail=false;;
"integer_values")
is_xfail=false
str_oracle=$(echo ${str_oracle} | sed -e 's/"val":"[0-9]\+"/"val":"ANYINT"/g')
str_out=$(echo ${str_out} | sed -e 's/"val":"[0-9]\+"/"val":"ANYINT"/g')
;;
*)
echo "High failure: unknown xfail value $is_xfail";
exit 2;;
esac
if [ "$str_oracle" = "$str_out" ] ; then
echo "ok"
else
if $updateoracle; then
echo "Updating oracle for $2, prover $1"
mv "$f.out" "$f.oracle"
echo "Updating oracle for ${file_path}, prover $1"
mv "$f.out" "${oracle_file}"
else
echo "FAILED!"
echo "Oracle is ${str_oracle}"
echo "Output is ${str_out}"
echo "diff is the following:"
diff "$f.oracle" "$f.out"
echo "$f"
diff "${oracle_file}" "$f.out"
if $is_xfail; then
echo "Failed but bench is ok because asserted as an XFAIL."
else
success=false
fi
fi
fi
}
for file in $files; do
filedir=`dirname $file`
filebase=`basename $file .mlw`
printf "Running provers on $filedir/$filebase.mlw\n";
run CVC4,1.5 $filedir/$filebase
run Z3,4.6.0 $filedir/$filebase
run CVC4,1.5 $filedir $filebase true
run CVC4,1.5 $filedir $filebase false
run Z3,4.6.0 $filedir $filebase true
run Z3,4.6.0 $filedir $filebase false
done
if $success; then
exit 0
......
bench/ce/algebraic_type_Z3,4.6.0.oracle deleted 100644 → 0
View file @ b5334af1
Weakest Precondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat)
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "1" },
{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat)
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "1" },
{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
bench/ce/algebraic_types_mono.mlw 0 → 100644
View file @ 43d39707
module M
use int.Int
type int_type = Integer int
goal G : forall x : int_type. match x with Integer y -> y > 0 end
type t = A | B int
goal g2: forall x. x = A
goal g4: forall x. x = B 0
type u = Au int int
goal g5: forall x. x = Au 0 0
type mylist = | Nil | Cons int mylist
let rec function len l = match l with
| Nil -> 0
| Cons _ l' -> 1 + len l'
end
goal g1: forall l: mylist. len l = 0
goal g7: forall l: mylist. l = Nil
end
bench/ce/array_mono.mlw 0 → 100644
View file @ 43d39707
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
bench/ce/bv32.mlw 0 → 100644
View file @ 43d39707
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
bench/ce/double_projection.mlw 0 → 100644
View file @ 43d39707
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
bench/ce/floats_CVC4,1.5.oracle deleted 100644 → 0
View file @ b5334af1
Weakest Precondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
Strongest Postcondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats_Z3,4.6.0.oracle deleted 100644 → 0
View file @ b5334af1
Weakest Precondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 5:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.000002p-126" ,
"value" : -1.17549e-38 } }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x0.008000p-127" ,
"value" : -1.14794e-41 } }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 9:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 13:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.000002p65" ,
"value" : 3.68935e+19 } }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 15:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 17:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 19:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 21:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x0.000002p-127" ,
"value" : 7.00649e-46 } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.99999ap-4" ,
"value" : 0.1 } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 31:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.0000000000001p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 33:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x0.0000040000000p-1023" ,
"value" : -2.65249e-315 } }
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 37:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 39:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.0000000000001p513" ,
"value" : 2.68156e+154 } }
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 41:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 43:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.0000000000000p54" ,
"value" : -1.80144e+16 } }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 45:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 49:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.999999999999ap-4" ,
"value" : 0.1 } }
Strongest Postcondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 5:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.000002p-126" ,
"value" : -1.17549e-38 } }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x0.008000p-127" ,
"value" : -1.14794e-41 } }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 9:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 13:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.000002p65" ,
"value" : 3.68935e+19 } }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 15:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 17:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 19:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 21:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x0.000002p-127" ,
"value" : 7.00649e-46 } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.99999ap-4" ,
"value" : 0.1 } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 31:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.0000000000001p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 33:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x0.0000040000000p-1023" ,
"value" : -2.65249e-315 } }
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 37:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 39:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.0000000000001p513" ,
"value" : 2.68156e+154 } }
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 41:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 43:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.0000000000000p54" ,
"value" : -1.80144e+16 } }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 45:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 49:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.999999999999ap-4" ,
"value" : 0.1 } }
bench/ce/if_assign.mlw 0 → 100644
View file @ 43d39707
module Test
use int.Int
use ref.Ref
val x : ref int
let f (a : int) : int
ensures { result = 0}
=
x := 42;
!x
let f2 (a : int) : int
ensures { result = 0}
=
x := 42;
!x
let f3 (a : int) : int
ensures { result = 0}
=
(if a = 0 then
x.contents <- 42
else
x := 18);
!x
let f4 (a : int) : int
ensures { result = 0}
=
(if a = 0 then
(x.contents <- 42; assert{ !x = 13})
else
(x := 18; assert { !x = 18}) );
17
end
bench/ce/if_decision_branch.mlw
View file @ 43d39707
......@@ -5,7 +5,7 @@ module Main
type path_sel_type = { mutable sel_path : bool}
val path_selector [@model] [@model_trace:TEMP_NAME]: path_sel_type
val path_selector [@model_trace:TEMP_NAME]: path_sel_type
end
......@@ -19,13 +19,15 @@ module Other
ensures {result = 5}
=
(* The counterexample should contain the node_id 5454 here but not 121 *)
if (([@node_id=5454] path_selector).sel_path <- (a = 1); path_selector.sel_path) then
if (path_selector.sel_path <- (a = 1); ([@branch_id=5454] path_selector).sel_path) then
5
else
begin path_selector.sel_path <- true;
(* The counterexample should contain the node_id 121 but not 5454 *)
if (([@node_id=121] path_selector).sel_path <- (a = 5); path_selector.sel_path) then
if (path_selector.sel_path <- (a = 5); ([@branch_id=121] path_selector).sel_path) then
15
else
22
end
end
bench/ce/if_decision_branch_CVC4,1.5.oracle deleted 100644 → 0
View file @ b5334af1
Weakest Precondition
bench/ce/if_decision_branch.mlw Other VC f: Valid
bench/ce/if_decision_branch.mlw Other VC f: Timeout or Unknown
Counter-example model:File if_decision_branch.mlw:
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "5" }
Line 19:
the check fails with all inputs
Line 22:
TEMP_NAME, [[@introduced], [@model],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
"val" : false }
Line 26:
TEMP_NAME, [[@introduced], [@model],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
"val" : true }
Strongest Postcondition
bench/ce/if_decision_branch.mlw Other VC f: Valid
bench/ce/if_decision_branch.mlw Other VC f: Timeout or Unknown
Counter-example model:File if_decision_branch.mlw:
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "5" }
Line 19:
the check fails with all inputs
bench/ce/if_decision_branch_Z3,4.6.0.oracle deleted 100644 → 0
View file @ b5334af1
Weakest Precondition
bench/ce/if_decision_branch.mlw Other VC f: Valid
bench/ce/if_decision_branch.mlw Other VC f: Unknown (sat)
Counter-example model:File if_decision_branch.mlw:
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 19:
the check fails with all inputs
Line 22:
TEMP_NAME, [[@introduced], [@model],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
"val" : false }
Line 26:
TEMP_NAME, [[@introduced], [@model],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
"val" : false }
Strongest Postcondition
bench/ce/if_decision_branch.mlw Other VC f: Valid
bench/ce/if_decision_branch.mlw Other VC f: Unknown (sat)
Counter-example model:File if_decision_branch.mlw:
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 19:
the check fails with all inputs
bench/ce/int32.mlw
View file @ 43d39707
module Ce_int32
use ref.Ref
use export mach.int.Int32
use mach.int.Int32
let dummy_update (r: ref int32)
requires { to_int !r = 22}
ensures {to_int !r = 42} =
r := of_int 42;
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
bench/ce/int32_CVC4,1.5.oracle deleted 100644 → 0
View file @ b5334af1
Weakest Precondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
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" }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
Line 9:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "42" }
Line 10:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
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" }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }