Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
126
Issues
126
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
33906b7e
Commit
33906b7e
authored
Nov 16, 2011
by
Tuyen Nguyen
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'master' of
git+ssh://scm.gforge.inria.fr//gitroot//why3/why3
parents
c8d03c30
1f652980
Changes
63
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
63 changed files
with
7669 additions
and
801 deletions
+7669
-801
META.in
META.in
+1
-1
Makefile.in
Makefile.in
+98
-74
ROADMAP
ROADMAP
+57
-19
configure.in
configure.in
+1
-25
drivers/cvc3_bare.drv
drivers/cvc3_bare.drv
+1
-1
drivers/tptp.drv
drivers/tptp.drv
+1
-1
drivers/vampire.drv
drivers/vampire.drv
+1
-1
examples/einstein/why3session.xml
examples/einstein/why3session.xml
+87
-12
examples/explicit_subst/why3session.xml
examples/explicit_subst/why3session.xml
+321
-1
examples/genealogy/why3session.xml
examples/genealogy/why3session.xml
+174
-36
examples/hello_proof/why3session.xml
examples/hello_proof/why3session.xml
+149
-4
examples/hoare_logic/imp_n/imp_n_Imp_consequence_rule_1.v
examples/hoare_logic/imp_n/imp_n_Imp_consequence_rule_1.v
+199
-0
examples/hoare_logic/wp.mlw
examples/hoare_logic/wp.mlw
+48
-45
examples/hoare_logic/wp/why3session.xml
examples/hoare_logic/wp/why3session.xml
+256
-30
examples/hoare_logic/wp/wp_WP_WP_WP_parameter_wp_1.v
examples/hoare_logic/wp/wp_WP_WP_WP_parameter_wp_1.v
+271
-0
examples/hoare_logic/wp_total.mlw
examples/hoare_logic/wp_total.mlw
+392
-0
examples/hoare_logic/wp_total/why3session.xml
examples/hoare_logic/wp_total/why3session.xml
+524
-0
examples/hoare_logic/wp_total/wp_total_Imp_If42_1.v
examples/hoare_logic/wp_total/wp_total_Imp_If42_1.v
+219
-0
examples/hoare_logic/wp_total/wp_total_Imp_Test55_1.v
examples/hoare_logic/wp_total/wp_total_Imp_Test55_1.v
+128
-0
examples/hoare_logic/wp_total/wp_total_Imp_assert_rule_1.v
examples/hoare_logic/wp_total/wp_total_Imp_assert_rule_1.v
+233
-0
examples/hoare_logic/wp_total/wp_total_Imp_assert_rule_ext_1.v
...les/hoare_logic/wp_total/wp_total_Imp_assert_rule_ext_1.v
+236
-0
examples/hoare_logic/wp_total/wp_total_Imp_assign_rule_1.v
examples/hoare_logic/wp_total/wp_total_Imp_assign_rule_1.v
+220
-0
examples/hoare_logic/wp_total/wp_total_Imp_eval_subst_1.v
examples/hoare_logic/wp_total/wp_total_Imp_eval_subst_1.v
+197
-0
examples/hoare_logic/wp_total/wp_total_Imp_eval_subst_2.v
examples/hoare_logic/wp_total/wp_total_Imp_eval_subst_2.v
+182
-0
examples/hoare_logic/wp_total/wp_total_Imp_eval_subst_term_1.v
...les/hoare_logic/wp_total/wp_total_Imp_eval_subst_term_1.v
+179
-0
examples/hoare_logic/wp_total/wp_total_Imp_if_rule_1.v
examples/hoare_logic/wp_total/wp_total_Imp_if_rule_1.v
+240
-0
examples/hoare_logic/wp_total/wp_total_Imp_many_steps_seq_1.v
...ples/hoare_logic/wp_total/wp_total_Imp_many_steps_seq_1.v
+249
-0
examples/hoare_logic/wp_total/wp_total_Imp_steps_non_neg_1.v
examples/hoare_logic/wp_total/wp_total_Imp_steps_non_neg_1.v
+207
-0
examples/hoare_logic/wp_total/wp_total_Imp_while_rule_1.v
examples/hoare_logic/wp_total/wp_total_Imp_while_rule_1.v
+263
-0
examples/hoare_logic/wp_total/wp_total_Imp_while_rule_ext_1.v
...ples/hoare_logic/wp_total/wp_total_Imp_while_rule_ext_1.v
+258
-0
examples/hoare_logic/wp_total/wp_total_WP_WP_WP_parameter_wp_1.v
...s/hoare_logic/wp_total/wp_total_WP_WP_WP_parameter_wp_1.v
+266
-0
examples/hoare_logic/wp_total/wp_total_WP_WP_WP_parameter_wp_2.v
...s/hoare_logic/wp_total/wp_total_WP_WP_WP_parameter_wp_2.v
+289
-0
examples/hoare_logic/wp_total/wp_total_WP_WP_WP_parameter_wp_3.v
...s/hoare_logic/wp_total/wp_total_WP_WP_WP_parameter_wp_3.v
+273
-0
examples/programs/decrease1/why3session.xml
examples/programs/decrease1/why3session.xml
+132
-57
examples/programs/ewd650.mlw
examples/programs/ewd650.mlw
+34
-0
examples/programs/ewd673.mlw
examples/programs/ewd673.mlw
+31
-0
examples/programs/ewd673/why3session.xml
examples/programs/ewd673/why3session.xml
+58
-0
examples/programs/vacid_0_binary_heaps/proofs/why3session.xml
...ples/programs/vacid_0_binary_heaps/proofs/why3session.xml
+354
-335
examples/programs/vstte10_max_sum/why3session.xml
examples/programs/vstte10_max_sum/why3session.xml
+82
-70
examples/test.equlin
examples/test.equlin
+0
-0
lib/coq/real/Abs.v
lib/coq/real/Abs.v
+0
-0
lib/coq/real/MinMax.v
lib/coq/real/MinMax.v
+0
-0
lib/coq/real/Real.v
lib/coq/real/Real.v
+0
-0
lib/coq/real/Square.v
lib/coq/real/Square.v
+0
-0
lib/plugins/.keepme
lib/plugins/.keepme
+0
-0
plugins/parser/genequlin.ml
plugins/parser/genequlin.ml
+5
-7
plugins/printer/tptpfof.ml
plugins/printer/tptpfof.ml
+3
-1
plugins/printer/tptpfof.mli
plugins/printer/tptpfof.mli
+0
-0
plugins/tptp/tptp_ast.ml
plugins/tptp/tptp_ast.ml
+121
-0
plugins/tptp/tptp_lexer.mli
plugins/tptp/tptp_lexer.mli
+20
-0
plugins/tptp/tptp_lexer.mll
plugins/tptp/tptp_lexer.mll
+318
-0
plugins/transform/.keepme
plugins/transform/.keepme
+0
-0
share/provers-detection-data.conf.in
share/provers-detection-data.conf.in
+24
-8
src/config.sh.in
src/config.sh.in
+1
-21
src/driver/autodetection.ml
src/driver/autodetection.ml
+14
-1
src/driver/driver.ml
src/driver/driver.ml
+2
-7
src/driver/whyconf.ml
src/driver/whyconf.ml
+1
-1
src/ide/gmain.ml
src/ide/gmain.ml
+1
-2
src/ide/replay.ml
src/ide/replay.ml
+8
-29
src/ide/session.ml
src/ide/session.ml
+9
-1
src/parser/lexer.mll
src/parser/lexer.mll
+0
-3
src/util/exn_printer.ml
src/util/exn_printer.ml
+0
-8
theories/set/Set.v
theories/set/Set.v
+231
-0
No files found.
META.in
View file @
33906b7e
...
...
@@ -2,4 +2,4 @@ description = "The Why3 Ocaml library"
version = "@VERSION@"
archive(byte) = "why3.cma"
archive(native) = "why3.cmxa"
requires = "str unix num
@META_DYNLINK@
@META_OCAMLGRAPH@"
requires = "str unix num
dynlink
@META_OCAMLGRAPH@"
Makefile.in
View file @
33906b7e
...
...
@@ -82,7 +82,7 @@ endif
# external libraries common to all binaries
EXTOBJS
=
EXTLIBS
=
str unix nums
@META_DYNLINK@
EXTLIBS
=
str unix nums
dynlink
EXTCMA
=
$(
addsuffix
.cma,
$(EXTLIBS)
)
$(
addsuffix
.cmo,
$(EXTOBJS)
)
EXTCMXA
=
$(
addsuffix
.cmxa,
$(EXTLIBS)
)
$(
addsuffix
.cmx,
$(EXTOBJS)
)
...
...
@@ -91,7 +91,7 @@ EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
# main target
###############
all
:
@OCAMLBEST@
all
:
@OCAMLBEST@
plugins
ifeq
(@enable_local@,yes)
all
:
install_local
...
...
@@ -133,7 +133,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
introduction abstraction close_epsilon lift_epsilon
\
eval_match instantiate_predicate smoke_detector
LIB_PRINTER
=
alt_ergo why3printer smtv1 smtv2 coq
tptp
simplify gappa
\
LIB_PRINTER
=
alt_ergo why3printer smtv1 smtv2 coq simplify gappa
\
cvc3 yices
LIBMODULES
=
src/config
\
...
...
@@ -208,7 +208,7 @@ clean::
install_no_local
::
mkdir
-p
$(BINDIR)
mkdir
-p
$(LIBDIR)
/why3
mkdir
-p
$(LIBDIR)
/why3
/coq
mkdir
-p
$(DATADIR)
/why3/images
mkdir
-p
$(DATADIR)
/why3/emacs
mkdir
-p
$(DATADIR)
/why3/lang
...
...
@@ -241,6 +241,84 @@ endif
install-all
:
install install-lib
##################
# Why plugins
##################
PLUGGENERATED
=
PLUG_PARSER
=
genequlin
PLUG_PRINTER
=
tptpfof
PLUG_TRANSFORM
=
PLUGINS
=
genequlin tptpfof
PLUGMODULES
=
$(
addprefix
plugins/parser/,
$(PLUG_PARSER)
)
\
$(
addprefix
plugins/printer/,
$(PLUG_PRINTER)
)
\
$(
addprefix
plugins/transform/,
$(PLUG_TRANSFORM)
)
PLUGML
=
$(
addsuffix
.ml,
$(PLUGMODULES)
)
PLUGMLI
=
$(
addsuffix
.mli,
$(PLUGMODULES)
)
PLUGCMO
=
$(
addsuffix
.cmo,
$(PLUGMODULES)
)
PLUGCMX
=
$(
addsuffix
.cmx,
$(PLUGMODULES)
)
PLUGDIRS
=
parser printer transform
PLUGINCLUDES
=
$(
addprefix
-I
plugins/,
$(PLUGDIRS)
)
$(PLUGCMO) $(PLUGCMX)
:
INCLUDES += $(PLUGINCLUDES)
plugins.byte
:
$(addsuffix .cmo
,
$(addprefix lib/plugins/
,
$(PLUGINS)))
plugins.opt
:
$(addsuffix .cmxs
,
$(addprefix lib/plugins/
,
$(PLUGINS)))
lib/plugins/%.cmxs
:
plugins/parser/%.cmx
$(
if
$(QUIET)
, @echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-shared
-o
$@
$<
lib/plugins/%.cmo
:
plugins/parser/%.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-pack
-o
$@
$<
lib/plugins/%.cmxs
:
plugins/printer/%.cmx
$(
if
$(QUIET)
, @echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-shared
-o
$@
$<
lib/plugins/%.cmo
:
plugins/printer/%.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-pack
-o
$@
$<
lib/plugins/%.cmxs
:
plugins/transform/%.cmx
$(
if
$(QUIET)
, @echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-shared
-o
$@
$<
lib/plugins/%.cmo
:
plugins/transform/%.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-pack
-o
$@
$<
include
.depend.plugins
.depend.plugins
:
$(PLUGGENERATED)
$(OCAMLDEP)
-slash
-I
src
-I
plugins
$(PLUGINCLUDES)
\
$(PLUGML)
$(PLUGMLI)
>
$@
depend
:
.depend.plugins
PLUGSDIRS
=
plugins
$(
addprefix
plugins/,
$(PLUGDIRS)
)
PLUGCLEAN
=
$(
addsuffix
/
*
.cm[iox],
$(PLUGSDIRS)
)
\
$(
addsuffix
/
*
.annot,
$(PLUGSDIRS)
)
\
$(
addsuffix
/
*
.output,
$(PLUGSDIRS)
)
\
$(
addsuffix
/
*
.automaton,
$(PLUGSDIRS)
)
\
$(
addsuffix
/
*
.o,
$(PLUGSDIRS)
)
\
$(
addsuffix
/
*
~,
$(PLUGSDIRS)
)
clean
::
rm
-f
$(PLUGCLEAN)
$(PLUGGENERATED)
rm
-f
lib/plugins/
*
rm
-f
.depend.plugins
install_no_local
::
mkdir
-p
$(LIBDIR)
/why3/plugins
cp
-f
lib/plugins/
*
$(LIBDIR)
/why3/plugins
##################
# Why binary
...
...
@@ -297,7 +375,7 @@ src/realize.cmx: src/why3.cmxa
clean
::
rm
-f
src/realize.cm[iox] src/realize.annot src/realize.o
rm
-f
bin/
realize.byte bin/realize.opt bin/
realize
rm
-f
bin/
why3realize.byte bin/why3realize.opt bin/why3
realize
install_no_local
::
cp
-f
bin/why3realize.@OCAMLBEST@
$(BINDIR)
/why3realize
...
...
@@ -442,7 +520,6 @@ clean::
rm
-f
src/config/
*
.annot src/config/
*
~
rm
-f
src/config/
*
.output src/config/
*
.automaton
rm
-f
bin/why3config.byte bin/why3config.opt bin/why3config
rm
-f
.why.conf
rm
-f
.depend.config
local_config
:
bin/why3config.@OCAMLBEST@
...
...
@@ -808,22 +885,22 @@ $(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
# build targets
plugins.byte byte
:
plugins/whytptp.cmo
plugins.opt opt
:
plugins/whytptp.cmxs
plugins.byte byte
:
lib/
plugins/whytptp.cmo
plugins.opt opt
:
lib/
plugins/whytptp.cmxs
plugins/whytptp.cmxs
plugins/whytptp.cmo
:
EXTOBJS += $(MENHIRLIB)
plugins/whytptp.cmxs
plugins/whytptp.cmo
:
INCLUDES += $(MENHIRINC)
lib/plugins/whytptp.cmxs lib/
plugins/whytptp.cmo
:
EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/
plugins/whytptp.cmo
:
INCLUDES += $(MENHIRINC)
plugins/whytptp.cmxs
:
$(TPTPCMX)
lib/
plugins/whytptp.cmxs
:
$(TPTPCMX)
$(
if
$(QUIET)
, @echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-shared
-o
$@
$^
plugins/whytptp.cmo
:
$(TPTPCMO)
lib/
plugins/whytptp.cmo
:
$(TPTPCMO)
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-pack
-o
$@
$^
install_no_local
::
cp
-f
plugins/whytptp.cm
*
$(LIBDIR)
/why3
/
cp
-f
lib/plugins/whytptp.cm
*
$(LIBDIR)
/why3/plugins
/
# depend and clean targets
...
...
@@ -839,7 +916,7 @@ clean::
rm
-f
src/tptp2why/
*
.cm
*
src/tptp2why/
*
.o
rm
-f
src/tptp2why/
*
.annot src/tptp2why/
*
.conflicts
rm
-f
src/tptp2why/
*
.output src/tptp2why/
*
.automaton
rm
-f
plugins/whytptp.cm
*
plugins/whytptp.o
rm
-f
lib/plugins/whytptp.cm
*
lib/
plugins/whytptp.o
rm
-f
.depend.tptp2why
endif
...
...
@@ -921,7 +998,7 @@ install_local: bin/why3doc
# bench
########
.PHONY
:
bench test
comp_bench_plugins
.PHONY
:
bench test
bench
::
bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
$(MAKE)
test-api
...
...
@@ -929,18 +1006,6 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ p
"bin/why3.@OCAMLBEST@"
\
"bin/why3ml.@OCAMLBEST@"
BENCH_PLUGINS_CMO
:=
helloworld.cmo
BENCH_PLUGINS_CMO
:=
$(
addprefix
bench/plugins/,
$(BENCH_PLUGINS_CMO)
)
BENCH_PLUGINS_CMXS
:=
$(BENCH_PLUGINS_CMO:.cmo=.cmxs)
comp_bench_plugins
::
$(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)
# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
# bin/why3.byte -D bench/plugins/helloworld.drv \
# tests/test-jcf.why -T Test -G G
# bin/why3.$(OCAMLBEST) -D bench/plugins/helloworld.drv \
# tests/test-jcf.why -T Test -G G
###############
# test targets
###############
...
...
@@ -991,51 +1056,6 @@ bts12244: src/why3.cma
ocaml
-I
src/
$(INCLUDES)
$(EXTCMA)
src/why3.cma examples/bts12244.ml
## Examples : Plugins ##
ifeq
(@enable_plugins@,yes)
PLUGDIR
=
examples/plugins/
PLUG_FILES
=
genequlin
PLUGMODULES
=
$(
addprefix
$(PLUGDIR)
,
$(PLUG_FILES)
)
PLUGML
=
$(
addsuffix
.ml,
$(PLUGMODULES)
)
PLUGCMO
=
$(
addsuffix
.cmo,
$(PLUGMODULES)
)
PLUGCMX
=
$(
addsuffix
.cmx,
$(PLUGMODULES)
)
PLUGCMXS
=
$(
addsuffix
.cmxs,
$(PLUGMODULES)
)
# ifeq (@enable_plug_support@,yes)
# byte: src/plug-plugin/whytac.cma
# opt: src/plug-plugin/whytac.cmxs
# endif
# $(PLUGCMO): src/why3.cma
# $(PLUGCMXS): src/why3.cmxa
.PHONY
:
examples_plugins.byte examples_plugins.opt
examples_plugins.byte
:
$(PLUGCMO)
examples_plugins.opt
:
$(PLUGCMXS)
# depend and clean targets
include
.depend.plug
.depend.plug
:
$(PLUGGENERATED)
$(OCAMLDEP)
-slash
-I
src
-I
$(PLUGDIR)
$(PLUGML)
|
sed
"s/cmx/cmxs/"
>
$@
depend
:
.depend.plug
clean
::
rm
-f
$(PLUGDIR)
/
*
.cm[iox]
$(PLUGDIR)
/
*
.o
rm
-f
$(PLUGDIR)
/
*
.cma
$(PLUGDIR)
/
*
.cmxs
rm
-f
$(PLUGDIR)
/
*
.annot
$(PLUGDIR)
/
*
~
rm
-f
$(PLUGGENERATED)
rm
-f
.depend.plug
endif
################
# documentation
################
...
...
@@ -1198,6 +1218,7 @@ DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
README INSTALL OCAML-LICENSE LICENSE
\
src/
*
.ml
*
src/
*
/
*
.ml
*
src/
*
/
*
.c
\
src/config.sh.in
\
plugins/
*
.ml
*
plugins/
*
/
*
.ml
*
\
doc/version.tex.in doc/manual.pdf
\
drivers/
*
.drv drivers/
*
.gen
\
examples/
*
.why examples/programs/
*
.mlw examples/tptp/
*
.why
\
...
...
@@ -1206,6 +1227,7 @@ DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
examples/use_api.ml
\
theories/
*
.why
\
modules/
*
.mlw
\
lib/coq/
*
/
*
.v
\
share/provers-detection-data.conf.in
\
share/emacs/why.el share/images/
*
.png share/lang/
*
.lang
...
...
@@ -1228,14 +1250,16 @@ $(DISTRIB_TAR): doc/manual.pdf
mkdir
-p
$(DISTRIB_DIR)
mkdir
-p
$(DISTRIB_DIR)
/bin
mkdir
-p
$(DISTRIB_DIR)
/share
mkdir
-p
$(DISTRIB_DIR)
/plugins
mkdir
-p
$(DISTRIB_DIR)
/lib
mkdir
-p
$(DISTRIB_DIR)
/lib/plugins
mkdir
-p
$(DISTRIB_DIR)
/lib/coq
ln
-s
../drivers
$(DISTRIB_DIR)
/share/drivers
ln
-s
../modules
$(DISTRIB_DIR)
/share/modules
ln
-s
../theories
$(DISTRIB_DIR)
/share/theories
cp
--parents
$(DISTRIB_FILES)
$(DISTRIB_DIR)
rm
-f
$(DISTRIB_DIR)
/src/config.ml
cd
$(DISTRIB_DIR)
;
rm
-f
$(LIBGENERATED)
$(TPTPGENERATED)
\
$(COQGENERATED)
$(WHY3DOCGENERATED)
$(COQGENERATED)
$(WHY3DOCGENERATED)
$(PLUGGENERATED)
cd
distrib
;
tar
cf
$(NAME)
.tar
$(NAME)
;
gzip
-f
--best
$(NAME)
.tar
# distrib export: source export-doc export-www export-examples export-examples-c linux
...
...
ROADMAP
View file @
33906b7e
...
...
@@ -8,13 +8,6 @@
* more libraries (theories and modules)
* WhyML
** regions : strong update
** clone module
** ghost code
** extraction of Ocaml code
** logic symbols used in programs
* A true Jessie3 front-end ?
* traceability: Partially done
...
...
@@ -47,29 +40,73 @@
=== Roadmap for next release ========================
* fix support for newer Z3, CVC3 and Alt-Ergo, allow several version
* stages
** M1. preuve d'un petit compilateur, pas de pb de lieur,
eventuellement outils pour les preuves par recurrence
a la Leino, + fct size automatique
** M2. Lieur en Why3, POPLmark challenge. vers
un theorie et/ou un module réutilisable de lieurs
** (M2?) Stage Airbus, "TIP" avec Frama-C/Jessie ou WP/Why/Coq
besoin du plugin Coq?
* PRIORITAIRE, JCF et ANDREI, clone de module
** demarche: ecrire une API avec smart constructors garantissant
le bon typage, et clone sera en premier lieu un de ces constructors
** cas d'utilisation: range d'entiers de Jessie, Flottants -> double ou single
containeurs pour Adacore et Claire
NON PRIORITAIRE ?
** regions : strong update
** ghost code
** logic symbols used in programs
* extraction vers Caml
** PRIORITAIRE, JCF, ANDREI, besoin pour cours aux JFLA en janvier 2012
* FRANCOIS new tools
** merge why3html and why3stats into a new executable why3report
** move -latex from why3replayer to why3report
** document why3report
* FRANCOIS
** document smoke detector
* CLAUDE provers
** fix support for newer Z3, CVC3 and Alt-Ergo, allow several version
of them at the same time. Allow why3config --detect to find e.g z3
under names like z3-3.2 (how ? command-line option ? e.g. -p z3 /usr/local/bin/z3-3.2)
** Ensure that we kill a prover after some time (ressurect %T ? with a
meaning like twice the value of %t ?), because we cannot be sure they always
honor their own -timeout option.
* FRANCOIS CLAUDE, move Session module and its dependencies into the Why3 library
** but avoid duplication with session_ro
** avoid also duplication of type like prover_data record
** do not include task and transf in the data type, so that
one can reload, and redetect provers
** session + session_ro -> session_data + session_dynamic
* move Session module and its dependencies into the Why3 library
* document new tools why3stats or others
* efficiency issues
** understand problems when large number of goals (cf D Mentré examples)
* Ensure that we kill a prover after some time (ressurect %T ? with a
meaning like twice the value of %t ?), because we cannot be sure they always
honor their own -timeout option.
* ALL fix bug and update the BTS
** reject global "val"s in typing environment for logic decls.
*
update the BTS
*
DELAYED Coq plugin
* API for programs
* Coq realization of theories
** corriger l'incoherence, comprendre si on veut vraiment accepter
* reject global "val"s in typing environment for logic decls.
function x : 'a
(cf: en caml cela ne marche pas)
* Coq plugin
** make it really usable
** understand problems when trying to realize set.why.
Status of equality, relation with clone module feature
* Coq realization of theories
* DOC:
** document new tools why3stats and others if any
** complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F)
...
...
@@ -79,9 +116,10 @@
** saving session
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
* do not save if no change was made
** restore provers detection in the middle of a session.
+ todo: run detection immediately at start up if conf file absent or
outdated
outdated
. should become doable with the new Session module
=== Roadmap for release 0.71 ========================
...
...
configure.in
View file @
33906b7e
...
...
@@ -17,10 +17,9 @@
# #
##########################################################################
#
# autoconf input for Objective Caml programs
# Copyright (C) 2001 Jean-Christophe Fillitre
# Copyright (C) 2001 Jean-Christophe Filli
â
tre
# from a first script by Georges Mariano
#
# This library is free software; you can redistribute it and/or
...
...
@@ -78,12 +77,6 @@ AC_ARG_ENABLE(bench,
[ --enable-bench enable Why3 benchmarking tool],,
enable_bench=yes)
# dynlink
AC_ARG_ENABLE(plugins,
[ --enable-plugins enable Why3 plugins],,
enable_plugins=yes)
# Coq plugin
AC_ARG_ENABLE(coq-support,
...
...
@@ -152,12 +145,6 @@ case "$OCAMLVERSION" in
AC_MSG_ERROR(You need Objective Caml 3.11.2 or higher);;
esac
if test "$enable_plugins" = "yes" ; then
DYNLINK="Dynlink"
else
DYNLINK="Dynlink_"
fi
# Ocaml library path
# old way: OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d ' ' | tr -d '\\r'`
OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
...
...
@@ -433,13 +420,6 @@ else
META_OCAMLGRAPH=""
fi
if test "$enable_plugins" = yes; then
META_DYNLINK="dynlink"
else
META_DYNLINK=""
fi
#Viewer for ps and pdf
dnl AC_CHECK_PROGS(PSVIEWER,gv evince)
dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
...
...
@@ -482,9 +462,6 @@ AC_SUBST(MENHIRLIB)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(SQLITE3LIB)
AC_SUBST(enable_bench)
AC_SUBST(enable_plugins)
AC_SUBST(DYNLINK)
AC_SUBST(META_DYNLINK)
AC_SUBST(META_OCAMLGRAPH)
AC_SUBST(enable_coq_support)
...
...
@@ -532,7 +509,6 @@ echo "Verbose make : $enable_verbose_make"
echo "Why IDE : $enable_ide $reason_ide"
echo "Why bench tool : $enable_bench"
echo "Why documentation : $enable_doc"
echo "Why plugins : $enable_plugins"
echo "Coq plugin support : $enable_coq_support $reason_coq_support"
if test "$enable_coq_support" = "yes" ; then
echo " Version : $COQVERSION"
...
...
drivers/cvc3_bare.drv
View file @
33906b7e
...
...
@@ -16,7 +16,7 @@ time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_
definit
ion"
transformation "eliminate_
recurs
ion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
...
...
drivers/tptp.drv
View file @
33906b7e
(* Why driver for first-order tptp provers *)
printer "tptp"
printer "tptp
-fof
"
filename "%f-%t-%g.p"
valid "Proof found"
...
...
drivers/vampire.drv
View file @
33906b7e
(* Why driver for first-order tptp provers *)
printer "tptp"
printer "tptp
-fof
"
filename "%f-%t-%g.p"
valid "Refutation found"
...
...
examples/einstein/why3session.xml
View file @
33906b7e
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name=
"e
xamples/e
instein/why3session.xml"
>
name=
"einstein/why3session.xml"
>
<prover
id=
"alt-ergo"
name=
"Alt-Ergo"
version=
"0.93"
/>
<prover
id=
"alt-ergo-0.93.1"
name=
"Alt-Ergo"
version=
"0.93.1"
/>
<prover
id=
"coq"
name=
"Coq"
...
...
@@ -14,6 +18,10 @@
id=
"cvc3"
name=
"CVC3"
version=
"2.2"
/>
<prover
id=
"cvc3-2.4"
name=
"CVC3"
version=
"2.4.1"
/>
<prover
id=
"eprover"
name=
"Eprover"
...
...
@@ -46,6 +54,10 @@
id=
"z3"
name=
"Z3"
version=
"2.19"
/>
<prover
id=
"z3-3"
name=
"Z3"
version=
"3.2"
/>
<file
name=
"../einstein.why"
verified=
"false"
...
...
@@ -75,16 +87,30 @@
proved=
"true"
expanded=
"true"
shape=
"ainfix =ato_aFishaGerman"
>
<proof
prover=
"alt-ergo-0.93.1"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"unknown"
time=
"0.45"
/>
</proof>
<proof
prover=
"z3-3"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.05"
/>
</proof>
<proof
prover=
"cvc3"
timelimit=
"
3
"
timelimit=
"
10
"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"2.
53
"
/>
<result
status=
"valid"
time=
"2.
42
"
/>
</proof>
<proof
prover=
"z3"
timelimit=
"
3
"
timelimit=
"
10
"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
...
...
@@ -96,6 +122,13 @@
obsolete=
"false"
>
<result
status=
"timeout"
time=
"4.96"
/>
</proof>
<proof
prover=
"cvc3-2.4"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"1.92"
/>
</proof>
<proof
prover=
"yices"
timelimit=
"3"
...
...
@@ -124,19 +157,33 @@
proved=
"false"
expanded=
"true"
shape=
"ainfix =ato_aCatsaSwede"
>
<proof
prover=
"alt-ergo-0.93.1"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"unknown"
time=
"0.43"
/>
</proof>
<proof
prover=
"z3-3"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"10.09"
/>
</proof>
<proof
prover=
"cvc3"
timelimit=
"
3
"
timelimit=
"
10
"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"
5.04
"
/>
<result
status=
"timeout"
time=
"
10.06
"
/>
</proof>
<proof
prover=
"z3"
timelimit=
"
3
"
timelimit=
"
10
"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"
3.02
"
/>
<result
status=
"timeout"
time=
"
10.09
"
/>
</proof>
<proof
prover=
"eprover"
...
...
@@ -145,6 +192,13 @@
obsolete=
"false"
>
<result
status=
"timeout"
time=
"4.97"
/>
</proof>
<proof
prover=
"cvc3-2.4"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"10.10"
/>
</proof>
<proof
prover=
"yices"
timelimit=
"3"
...
...
@@ -173,19 +227,33 @@
proved=
"true"
expanded=
"true"
shape=
"ainfix =ato_aCatsaNorwegian"
>
<proof
prover=
"alt-ergo-0.93.1"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"unknown"
time=
"0.43"
/>
</proof>
<proof
prover=
"z3-3"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.05"
/>
</proof>
<proof
prover=
"cvc3"
timelimit=
"
3
"
timelimit=
"
10
"