Skip to content

GitLab

why3
why3
Commit 2bf9572e authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Merge branch 'next' into new_ide

parents 971bea60 9aed1fbc
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 746 additions and 770 deletions
.gitattributes
View file @ 2bf9572e
.gitattributes export-ignore
.gitignore export-ignore
.keepme export-ignore
/.gitlab-ci.yml export-ignore
/.mailmap export-ignore
......
CHANGES.md
View file @ 2bf9572e
......@@ -2,21 +2,21 @@
Provers
* support for Alt-Ergo 2.0.0 (released Nov 14, 2017)
* support for Coq 8.7.1 (released Dec 16, 2017)
* support for Z3 4.6.0 (released Dec 18, 2017)
Standard library
* fix compatibility of theory int.Exponentiation with instances
where multiplication is not commutative.
fix corresponding realizations in Coq and Isabelle/HOL :x:
* fixed soundness of theory `int.Exponentiation` when multiplication is not
commutative :x:
Bug fixes
* Fix issue #50:
share/Makefile.config is missing when enable_relocation=yes
Miscellaneous
* fixed support for `--enable_relocation=yes` (issue #50)
* fixed support for Windows (issue #70)
Version 0.88.2, December 7, 2017
--------------------------------
Bug fixes
Miscellaneous
* `why3 session html`: improved compliance of generated files
* `why3 doc`: fixed missing anchors for operator definitions
* improved build process when `coqtop.byte` is missing
......
Makefile.in
View file @ 2bf9572e
......@@ -261,12 +261,12 @@ endif
# hide deprecated warnings for strings
src/util/strings.cmo:: WARNINGS:=$(WARNINGS)-3
src/util/strings.cmx:: WARNINGS:=$(WARNINGS)-3
src/util/strings.cmo: WARNINGS:=$(WARNINGS)-3
src/util/strings.cmx: WARNINGS:=$(WARNINGS)-3
# hide warning 'no cmx file was found in path for module ..., and its interface was not compiled with -opaque' for the coq tactic
src/coq-tactic/why3tac.cmx:: WARNINGS:=$(WARNINGS)-58
src/coq-tactic/why3tac.cmx: WARNINGS:=$(WARNINGS)-58
# build targets
......@@ -451,45 +451,27 @@ LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))
plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
lib/plugins/%.cmxs: plugins/parser/%.cmx
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
lib/plugins:
mkdir lib/plugins
lib/plugins/%.cmo: plugins/parser/%.cmo
lib/plugins/%.cmxs: | lib/plugins
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/%.cmxs: plugins/printer/%.cmx
lib/plugins/%.cmo: | lib/plugins
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/plugins/%.cmxs: plugins/parser/%.cmx
lib/plugins/%.cmo: plugins/parser/%.cmo
lib/plugins/%.cmxs: plugins/printer/%.cmx
lib/plugins/%.cmo: plugins/printer/%.cmo
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/%.cmxs: plugins/transform/%.cmx
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
lib/plugins/%.cmo: plugins/transform/%.cmo
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/tptp.cmxs: $(TPTPCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/tptp.cmo: $(TPTPCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/plugins/python.cmxs: $(PYTHONCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/python.cmo: $(PYTHONCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
# depend and clean targets
......@@ -531,6 +513,9 @@ $(TOOLSDEP): $(TOOLSGENERATED)
byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt: bin/why3.opt $(TOOLS_BIN:%=bin/%.opt)
bin:
mkdir bin
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
bin/why3config.opt: lib/why3/why3.cmxa src/tools/why3config.cmx
......@@ -744,14 +729,10 @@ opt: bin/why3ide.opt
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.byte: BLINKFLAGS += -custom
bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
src/ide/resetgc.o: src/ide/resetgc.c
$(SHOW) 'Ocamlc $<'
......@@ -850,12 +831,7 @@ byte: bin/why3session.byte
opt: bin/why3session.opt
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
......@@ -1572,12 +1548,7 @@ byte: bin/why3doc.byte
opt: bin/why3doc.opt
bin/why3doc.opt: lib/why3/why3.cmxa $(WHY3DOCCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3doc.byte: lib/why3/why3.cma $(WHY3DOCCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
......@@ -1942,7 +1913,8 @@ apidot: doc/apidoc/dg.svg doc/apidoc/dg.png
doc/apidoc/dg.dot: doc/apidoc $(FILESTODOC)
$(OCAMLDOC) -o doc/apidoc/dg.dot.tmp -dot $(INCLUDES) \
$(LIBINCLUDES) -I lib/why3 $(FILESTODOC)
sed -e "s/ \(size\|ratio\|rotate\|fontsize\).*$$//" doc/apidoc/dg.dot.tmp > doc/apidoc/dg.dot
sed -e "s/ \(size\|ratio\|rotate\|fontsize\).*$$//" doc/apidoc/dg.dot.tmp \
| tred > doc/apidoc/dg.dot
rm -f doc/apidoc/dg.dot.tmp
doc/apidoc/dg.svg: doc/apidoc/dg.dot
......@@ -2101,11 +2073,11 @@ src/tools/why3extract.cmx: %.cmx: %.ml
echo '$*.cmx : $*.cmi'; \
echo '$*.cmi : $*.cmo') $(TOTARGET)
%.opt:
bin/%.opt: | bin
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
%.byte:
bin/%.byte: | bin
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
......
doc/fix.hva
View file @ 2bf9572e
......@@ -5,7 +5,7 @@
\newcommand{\vfill}{}
\newcommand{\hrulefill}{}
\newcommand{\null}{}
\newcommand{\path}[1]{\texttt{#1}}
\def\path{\begingroup\urlstyle{tt}\Url}
\renewcommand{\framebox}[1]{#1}
\makeatletter
......
examples/WP_revisited/imp_n/why3session.xml
View file @ 2bf9572e
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.7.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -33,34 +33,34 @@
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="progress" expl="">
<proof prover="2" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="0" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="steps_non_neg" expl="">
<proof prover="2" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="many_steps_seq" expl="">
<proof prover="2" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
<proof prover="0" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="eval_subst_expr" expl="">
<proof prover="2" edited="imp_n_Imp_eval_subst_expr_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="0" edited="imp_n_Imp_eval_subst_expr_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="eval_subst" expl="">
<proof prover="2" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.35"/></proof>
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="skip_rule" expl="">
<proof prover="6"><result status="valid" time="0.04" steps="113"/></proof>
</goal>
<goal name="assign_rule" expl="">
<proof prover="2" edited="imp_n_Imp_assign_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_assign_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="seq_rule" expl="">
<proof prover="2" edited="imp_n_Imp_seq_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_seq_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="if_rule" expl="">
<proof prover="2" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="while_rule" expl="">
<proof prover="2" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="consequence_rule" expl="">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......
examples/WP_revisited/wp2/why3session.xml
View file @ 2bf9572e
......@@ -2,26 +2,26 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../wp2.mlw" expanded="true">
<theory name="Imp" sum="4d6ec4c3ea3a39365f84600c953b8179">
<goal name="eval_subst_term" expl="">
<proof prover="1" timelimit="5" edited="wp2_Imp_eval_subst_term_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_subst_term_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="eval_term_change_free" expl="">
<proof prover="1" timelimit="5" edited="wp2_Imp_eval_term_change_free_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_term_change_free_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="eval_subst" expl="">
<proof prover="1" timelimit="5" edited="wp2_Imp_eval_subst_1.v"><result status="valid" time="0.37"/></proof>
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_subst_1.v"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="eval_swap" expl="">
<proof prover="2" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="eval_change_free" expl="">
<proof prover="1" timelimit="5" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="check_skip" expl="">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -29,10 +29,10 @@
<proof prover="7" memlimit="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="steps_non_neg" expl="">
<proof prover="1" edited="wp2_Imp_steps_non_neg_1.v"><result status="valid" time="0.36"/></proof>
<proof prover="0" edited="wp2_Imp_steps_non_neg_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="many_steps_seq" expl="">
<proof prover="1" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="0.41"/></proof>
<proof prover="0" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="0.41"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="ea9fb18b1935c25df0ce7f228aabf76f">
......@@ -49,14 +49,14 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="Test55" expl="">
<proof prover="1" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_Test55_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="0" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_Test55_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="Ass42" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.04"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.06" steps="100"/></proof>
</goal>
<goal name="If42" expl="">
<proof prover="1" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_If42_1.v"><result status="valid" time="1.00"/></proof>
<proof prover="0" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_If42_1.v"><result status="valid" time="1.00"/></proof>
</goal>
</theory>
<theory name="HoareLogic" sum="ac7395abbc54f2eaf2a4731bbadf3a7c">
......@@ -64,28 +64,28 @@
<proof prover="2" memlimit="1000"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="skip_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_skip_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="wp2_HoareLogic_skip_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="assign_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_assign_rule_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="0" edited="wp2_HoareLogic_assign_rule_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="seq_rule" expl="">
<proof prover="5" timelimit="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="if_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_if_rule_1.v"><result status="valid" time="0.48"/></proof>
<proof prover="0" edited="wp2_HoareLogic_if_rule_1.v"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="assert_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_assert_rule_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="0" edited="wp2_HoareLogic_assert_rule_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="assert_rule_ext" expl="">
<proof prover="1" edited="wp2_HoareLogic_assert_rule_ext_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="0" edited="wp2_HoareLogic_assert_rule_ext_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="while_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="0.52"/></proof>
<proof prover="0" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="while_rule_ext" expl="">
<proof prover="1" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="0.54"/></proof>
<proof prover="0" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="0.54"/></proof>
</goal>
</theory>
<theory name="WP" sum="ac7e95b3f1136de0ba1a9054f4091dbf">
......@@ -107,7 +107,7 @@
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.06" steps="94"/></proof>
</goal>
<goal name="WP_parameter compute_writes.2" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_compute_writes_1.v"><result status="valid" time="0.38"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_1.v"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="WP_parameter compute_writes.3" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="42"/></proof>
......@@ -125,16 +125,16 @@
<proof prover="7"><result status="valid" time="0.04" steps="48"/></proof>
</goal>
<goal name="WP_parameter compute_writes.8" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_compute_writes_3.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_3.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="WP_parameter compute_writes.9" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="WP_parameter compute_writes.10" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_compute_writes_4.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_4.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="WP_parameter compute_writes.11" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_compute_writes_2.v"><result status="valid" time="0.34"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_2.v"><result status="valid" time="0.34"/></proof>
</goal>
</transf>
</goal>
......@@ -168,7 +168,7 @@
<proof prover="7"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
<goal name="WP_parameter wp.8" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_wp_1.v"><result status="valid" time="0.32"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_wp_1.v"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="WP_parameter wp.9" expl="postcondition">
<proof prover="2" timelimit="3"><result status="valid" time="0.04"/></proof>
......@@ -179,7 +179,7 @@
<proof prover="7"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="WP_parameter wp.11" expl="postcondition">
<proof prover="1" timelimit="5" edited="wp2_WP_WP_WP_parameter_wp_2.v"><result status="valid" time="0.87"/></proof>
<proof prover="0" timelimit="5" edited="wp2_WP_WP_WP_parameter_wp_2.v"><result status="valid" time="0.87"/></proof>
</goal>
</transf>
</goal>
......
examples/bellman_ford/why3session.xml
View file @ 2bf9572e
This diff is collapsed.
examples/bitvectors/bitvector/why3session.xml
View file @ 2bf9572e
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -31,16 +31,16 @@
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="to_nat_of_zero2" expl="">
<proof prover="0" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="to_nat_of_zero" expl="">
<proof prover="0" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.01"/></proof>
<proof prover="1" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.01"/></proof>
</goal>
<goal name="to_nat_of_one" expl="">
<proof prover="0" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="0.96"/></proof>
<proof prover="1" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="0.96"/></proof>
</goal>
<goal name="to_nat_sub_footprint" expl="">
<proof prover="0" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="1.22"/></proof>
<proof prover="1" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="1.48"/></proof>
</goal>
<goal name="nth_from_int_low_even" expl="">
<proof prover="2"><result status="valid" time="0.02" steps="68"/></proof>
......@@ -72,7 +72,7 @@
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="nth_from_int2c_plus_pow2" expl="">
<proof prover="0" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.51"/></proof>
<proof prover="1" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.75"/></proof>
<proof prover="2"><result status="valid" time="0.33" steps="94"/></proof>
</goal>
</theory>
......
examples/bitvectors/double/why3session.xml
View file @ 2bf9572e
......@@ -4,8 +4,8 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -28,7 +28,7 @@
</goal>
<goal name="exp_one" expl="" expanded="true">
<proof prover="0" timelimit="30"><result status="valid" time="2.23" steps="668"/></proof>
<proof prover="2" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.38"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="mantissa_one" expl="">
<proof prover="0"><result status="valid" time="0.09" steps="87"/></proof>
......
examples/bitvectors/double_of_int/why3session.xml
View file @ 2bf9572e
......@@ -5,8 +5,8 @@
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.7.1" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double_of_int.why" expanded="true">
......@@ -86,7 +86,7 @@
<proof prover="8"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="exp_const" expl="">
<proof prover="3" timelimit="30" edited="double_of_int_DoubleOfInt_exp_const_1.v"><result status="valid" time="0.80"/></proof>
<proof prover="5" timelimit="30" edited="double_of_int_DoubleOfInt_exp_const_1.v"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="to_nat_mantissa_1" expl="">
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
......@@ -162,10 +162,10 @@
<proof prover="8"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_pos" expl="">
<proof prover="3" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.76"/></proof>
<proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.76"/></proof>
</goal>
<goal name="lemma1_pos" expl="">
<proof prover="3" timelimit="6" edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"><result status="valid" time="1.39"/></proof>
<proof prover="5" timelimit="6" edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"><result status="valid" time="1.39"/></proof>
</goal>
<goal name="jpxorx_neg" expl="">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -174,10 +174,10 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_neg" expl="">
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="1.74"/></proof>
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="1.74"/></proof>
</goal>
<goal name="lemma1_neg" expl="">
<proof prover="3" timelimit="10" edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"><result status="valid" time="0.52"/></proof>
<proof prover="5" timelimit="10" edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="lemma1" expl="">
<proof prover="1"><result status="valid" time="0.06" steps="95"/></proof>
......@@ -190,7 +190,7 @@
<proof prover="4" timelimit="10"><result status="valid" time="1.98"/></proof>
</goal>
<goal name="to_nat_bv32_bv64_aux" expl="">
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="1.74"/></proof>
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="1.74"/></proof>
</goal>
<goal name="to_nat_bv32_bv64" expl="">
<proof prover="1"><result status="valid" time="0.06" steps="90"/></proof>
......@@ -213,7 +213,7 @@
<proof prover="8"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="lemma2" expl="">
<proof prover="3" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="23.13"/></proof>
<proof prover="5" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="18.61"/></proof>
</goal>
<goal name="nth_var4" expl="">
<proof prover="1"><result status="valid" time="1.14" steps="148"/></proof>
......@@ -267,7 +267,7 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="var_value0" expl="">
<proof prover="3" timelimit="30" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.14"/></proof>
<proof prover="5" timelimit="30" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.14"/></proof>
</goal>
<goal name="from_int_sum" expl="">
<proof prover="1"><result status="valid" time="0.05" steps="92"/></proof>
......
examples/bitvectors/power2/why3session.xml
View file @ 2bf9572e
......@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -18,10 +18,10 @@
<proof prover="10"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="Power_sum" expl="">
<proof prover="1" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.61"/></proof>
<proof prover="4" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.61"/></proof>
</goal>
<goal name="pow2pos" expl="">
<proof prover="1" edited="power2_Pow2int_pow2pos_1.v"><result status="valid" time="0.49"/></proof>
<proof prover="4" edited="power2_Pow2int_pow2pos_1.v"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="pow2_0" expl="">
<proof prover="0"><result status="valid" time="0.00"/></proof>
......@@ -431,7 +431,7 @@
<proof prover="10"><result status="valid" time="0.24" steps="99"/></proof>
</goal>
<goal name="Mod_pow2_gen" expl="">
<proof prover="1" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
<proof prover="4" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
</goal>
</theory>
<theory name="Pow2real" sum="129a1971aba7e377549f155f30711f18" expanded="true">
......@@ -467,25 +467,25 @@
<proof prover="10"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Power_non_null_aux" expl="">
<proof prover="1" edited="power2_Pow2real_Power_non_null_aux_1.v"><result status="valid" time="0.65"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_non_null_aux_1.v"><result status="valid" time="0.65"/></proof>
</goal>
<goal name="Power_neg_aux" expl="">
<proof prover="1" edited="power2_Pow2real_Power_neg_aux_1.v"><result status="valid" time="0.68"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_neg_aux_1.v"><result status="valid" time="0.68"/></proof>
</goal>
<goal name="Power_non_null" expl="">
<proof prover="1" edited="power2_Pow2real_Power_non_null_1.v"><result status="valid" time="0.64"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_non_null_1.v"><result status="valid" time="0.81"/></proof>
</goal>
<goal name="Power_neg" expl="">
<proof prover="10"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="Power_sum_aux" expl="">
<proof prover="1" edited="power2_Pow2real_Power_sum_aux_1.v"><result status="valid" time="0.62"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_sum_aux_1.v"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="Power_sum" expl="">
<proof prover="1" edited="power2_Pow2real_Power_sum_1.v"><result status="valid" time="0.62"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_sum_1.v"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="Pow2_int_real" expl="">
<proof prover="1" edited="power2_Pow2real_Pow2_int_real_1.v"><result status="valid" time="0.51"/></proof>
<proof prover="4" edited="power2_Pow2real_Pow2_int_real_1.v"><result status="valid" time="0.51"/></proof>
</goal>
</theory>
</file>
......
examples/bresenham/why3session.xml
View file @ 2bf9572e
......@@ -2,15 +2,15 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../bresenham.mlw" expanded="true">
<theory name="M" sum="3da6ad55dc32260aace6cf777010522a" expanded="true">
<goal name="closest" expl="" expanded="true">
<proof prover="2" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
<proof prover="0" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="WP_parameter bresenham" expl="VC for bresenham" expanded="true">
<transf name="split_goal_wp" expanded="true">
......
examples/bts/12934/why3session.xml
View file @ 2bf9572e
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../12934.why" expanded="true">
<theory name="BTS12934" sum="e32351513bba9a37f680056dd466bcee" expanded="true">
<goal name="t" expl="" expanded="true">
<proof prover="1" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
<proof prover="0" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
</goal>
</theory>
</file>
......
examples/bts/13849/why3session.xml
View file @ 2bf9572e
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../13849.why" expanded="true">
<theory name="T" sum="fe6d0a97ed129807ad9b025e583a359d" expanded="true">
<goal name="x" expl="" expanded="true">
<proof prover="1" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
<proof prover="0" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
</goal>
</theory>
</file>
......
examples/bts/13854/why3session.xml
View file @ 2bf9572e
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">