Merge commit '680be27a' into counter-examples

Conflicts:
	drivers/cvc4_bare.drv
	share/provers-detection-data.conf
	src/driver/driver_parser.mly
	src/printer/smtv2.ml

CHANGES

 
 * marks an incompatible change
 
+core
+  o steps limit for reliable replay of proofs, available for Alt-Ergo
+    and CVC4
+  o new transformations induction_pr and inversion_pr to reason with
+    inductive predicates
+
 library
-  * renamed library int.NumOfParam into int.NumOf; the predicate numof
+  * renamed theory int.NumOfParam into int.NumOf; the predicate numof
     now takes some higher-order predicate as argument (no more need
     for cloning). Similar change in modules array.NumOf...
+  * improved theory real.PowerReal
+  o new theory: sequences
+  o new theories for bitvectors, mapped to BV theories of SMT solvers
+    Z3 and CVC4
 
 provers
   o support for Coq 8.4pl5 (released Nov 7, 2014)
   o support for Z3 4.3.2 (released Oct 25, 2014)
   o support for MetiTarski 2.4 (released Oct 21, 2014)
   o support for Alt-Ergo 0.99.1 (released Dec 30, 2014)
+  o support for Alt-Ergo 1.00.prv (released Jan 29, 2015)
+  o support for veriT 201410 (released Nov 2014)
+  o support for Psyche (experimental,
+    http://www.lix.polytechnique.fr/~lengrand/Psyche/)
+  o preliminary support for upcoming CVC4 1.5 (steps feature)
+
+bug fixes:
+  o bug in interpreter in presence of nested mutable fields
+  o IDE: proofs in progress should never be "cleaned"
+  o IDE: display warnings after reload
+
+IDE:
+  o conf file not automatically saved anymore at exit
+  o right part of main window organized in tabs
 
 version 0.85, September 17, 2014
 ================================

Makefile.in

 ####################################################################
 #                                                                  #
 #  The Why3 Verification Platform   /   The Why3 Development Team  #
-#  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  #
+#  Copyright 2010-2015   --   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  #
@@ -47,7 +47,8 @@ OCAMLBEST = @OCAMLBEST@
 OCAMLVERSION = @OCAMLVERSION@
 COQC      = @COQC@
 COQDEP    = @COQDEP@
-CAMLP5O   = @CAMLP5O@
+COQCAMLP  = @COQCAMLP@
+COQCAMLPLIB = @COQCAMLPLIB@
 FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
 
 ifeq (@enable_menhirLib@,yes)
@@ -119,9 +120,9 @@ CLEANLIBS =
 GENERATED =
 
 install_local::
-	ln -s ../drivers share/drivers
-	ln -s ../modules share/modules
-	ln -s ../theories share/theories
+	ln -s -n -f ../drivers share/drivers
+	ln -s -n -f ../modules share/modules
+	ln -s -n -f ../theories share/theories
 
 ##############
 # Why3 library
@@ -152,6 +153,7 @@ LIB_MLW = ity expr dexpr
 LIB_PARSER = ptree glob parser typing lexer
 
 LIB_TRANSFORM = simplify_formula inlining split_goal induction \
+		detect_polymorphism \
 		eliminate_definition eliminate_algebraic \
 		eliminate_inductive eliminate_let eliminate_if \
 		libencoding discriminate encoding encoding_select \
@@ -768,7 +770,7 @@ COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
 COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
 
 COQPTREES = kernel interp intf lib library parsing pretyping proofs printing tactics toplevel
-COQPINCLUDES = -I src/coq-tactic -I +camlp5 $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
+COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
 
 $(COQPDEP): DEPFLAGS += -I src/coq-tactic
 $(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
@@ -795,8 +797,8 @@ lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
 	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
 
 src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
-	$(if $(QUIET),@echo 'Camlp5   $<' &&) \
-	    $(CAMLP5O) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
+	$(if $(QUIET),@echo 'Camlp    $<' &&) \
+	    $(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
 
 src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
 	$(if $(QUIET),@echo 'Coqc     $<' &&) \
@@ -845,7 +847,7 @@ COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
 COQLIBS_BOOL_FILES = Bool
 COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES))
 
-COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt Real RealInfix Square Trigonometry
+COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry
 COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
 
 COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
@@ -919,7 +921,7 @@ ifeq (@enable_coq_fp_libs@,yes)
 	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
 endif
 
-update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp
+update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp headers-coq
 
 update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
 	for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
@@ -1814,13 +1816,19 @@ dist: $(EXTRA_DIST)
 # file headers
 ###############
 
-headers:
+headers: headers-coq
 	headache -c misc/headache_config.txt -h misc/header.txt \
 		Makefile.in configure.in \
-		src/*/*.ml src/*/*.ml[iyl] \
-		plugins/*/*.ml plugins/*/*.ml[ily] src/tools/cpulimit.c \
+		src/*/*.ml src/*/*.ml[iyl4] \
+		plugins/*/*.ml plugins/*/*.ml[ily] \
+		lib/coq-tactic/*.v lib/coq/*.v \
+		src/tools/cpulimit.c \
 		examples/use_api/*.ml
 
+headers-coq:
+	headache -c misc/headache_config.txt -h misc/header.txt \
+		lib/coq/*/*.v
+
 #########
 # myself
 #########

ROADMAP

@@ -147,6 +147,167 @@ and no epsilon
    chaque instance necessaires. plutot qu'un seul symbole _match
    polymorphe.
 
+==================== Roadmap for release 0.86 ========================
+
+
+
+Release Notes (details in file CHANGES):
+
+* Support for new provers or new versions of provers
+
+
+== TODO ==
+
+determine which is the minumum version of Ocaml to compile, and then
+updated configure.in and the manual
+
+support for veriT recent
+-> DONE: version 201410
+
+support for Yices2 recent
+-> DONE: 2.3.0, but still does not support quantifiers
+
+solve issues with metitarski
+. DONE theory PowerReal
+. crashes when applied on a WP (see examples/my_cosine.mlw)
+
+clean up the support for SMTLIB bitvectors: there are 2 theories in the stdlib: thoeries/bv.why and modules/bitvectors.mlw
+
+decide if GUI with tabs is convenient enough
+
+== Final preparation ==
+
+* faire une passe sur le BTS
+* do "make update-coq" and "make", fix Coq realizations if needed
+* check that nightly bench is OK
+* check that "make xml-validate-local" is OK
+  (see below : copy the dtd on the web)
+* put 0.86 in file Version, and then run ./config.status
+* check/update the content of the About dialog in src/ide/gconfig.ml
+  around lines 550-600
+* check headers
+* check the file CHANGES, add the release date
+* manual in PDF:
+** update the date in doc/manual.tex (near \whyversion{})
+** check that macro \todo is commented out in doc/macros.tex
+** and then "make doc"
+  (check that manual in HTML is also generated, doc/html/index.html)
+* do "make dist"
+* test distrib/why3-0.86.tar.gz
+* put on the web page why3-0.86.tar.gz:
+  cp distrib/why3-0.86.tar.gz /users/www-perso/projets/why3/download
+* inform Jerry James <loganjerry@gmail.com> so that he can test the
+  Fedora package
+* install web page for why2 which includes an updated page for the
+  quick migration guide. (sources are in CVS repository
+  ~filliatr/ARCHIVE/www/why).
+* move distrib from Why3 site to Inria forge:
+** remove /users/www-perso/projets/why3/download/why3-0.86.tar.gz
+** upload distrib/why3-0.86.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
+* put on the web page
+ - the manual in PDF
+   cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.86.pdf
+
+ - the HTML version of the manual (content of doc/html)
+   cp -r doc/html /users/www-perso/projets/why3/doc-0.86
+
+ - why3session.dtd
+   cp -f share/why3session.dtd /users/www-perso/projets/why3/
+
+ - standard library online, using why3doc, to http://why3.lri.fr/stdlib/
+   make stdlibdoc
+   cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.86
+   rm /users/www-perso/projets/why3/stdlib
+   ln -s /users/www-perso/projets/why3/stdlib-0.86 \
+            /users/www-perso/projets/why3/stdlib
+ - API doc, produced using ocamldoc, to http://why3.lri.fr/api/
+    make apidoc
+    cp -r doc/apidoc /users/www-perso/projets/why3/api-0.86
+    rm /users/www-perso/projets/why3/api
+    ln -s /users/www-perso/projets/why3/api-0.86 \
+      /users/www-perso/projets/why3/api
+
+ - update the main HTML page (sources are in repository why3-www)
+   edit index.html
+   make (to check validity)
+   make export
+
+ - add links to extra resources like
+   http://why3.lri.fr/jfla-2012/, http://www.lri.fr/~marche/MPRI-2-36-1/,
+   page du cours de l'X (in french ? using Krakatoa/why3 bridge)
+
+ - make everything writeable for the group
+   chmod -R g+w /users/www-perso/projets/why3
+
+* prepare for the OPAM package
+
+. update opam/url: url and checksum of why-0.86.tar.gz
+   (use "md5sum distrib/why3-0.86.tar.gz")
+. update opam/descr if necessary
+. update opam/opam with correct dependencies and such
+
+* make a last commit:
+ - git commit -am "release 0.86"
+ - add tag 0.86 to the git repository, using
+   git tag 0.86
+ - do not forget to push it using
+   git push
+   git push --tags
+
+* add a new version to the bugtracker:
+  https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
+
+
+* test the OPAM package
+
+  . with opam 1.2:
+    opam pin add why3 --kind=git <...>/why3/.git
+    (it runs "opam install why3")
+  . with opam < 1.2:
+
+    - first step: have a local copy of opam-repository if not done yet, e.g.:
+
+        git clone git@github.com:claudemarche/opam-repository.git
+        cd opam-repository/
+        git remote add opam https://github.com/ocaml/opam-repository.git
+
+      or, if you already have one, make sure it is up-to-date:
+
+        git fetch opam
+        git reset --hard opam/master
+        git push
+
+    - second step: copy why3 opam files into it :
+
+      cd packages/why3
+      cp -r <source why3>/opam why3.0.86
+
+    - second step:
+
+      opam repository add local <...>/opam-repository
+      opam install why3
+      (* test it, e.g.
+         cp example/quicksort.mlw ~/tmp
+         why3 ide ~/tmp/quicksort.mlw *)
+      opam remove why3
+      opam repository remove local
+
+
+* make a pull request on OPAM
+
+  git add why3.0.86
+  git commit -am "new package version why3 0.86"
+  git push
+  sur github: creer un pull request
+
+* produce the Why3 part of Toccata gallery
+  -> add also a tar.gz and a ZIP file of it (this is done by doing
+  "make gallery-files" in the sources of the Toccata web pages)
+* Announce the distrib
+ - What to put in the announcement: see New Features above
+* The next commit : add +git to the version in file Version
+
+
 ==================== Roadmap for release 0.85 ========================
 
 Release Notes:

configure.in

 ####################################################################
 #                                                                  #
 #  The Why3 Verification Platform   /   The Why3 Development Team  #
-#  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  #
+#  Copyright 2010-2015   --   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  #
@@ -275,8 +275,6 @@ if test "$MENHIR" = no ; then
 	AC_MSG_ERROR(Cannot find menhir.)
 fi
 
-AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)
-
 ## Where are the library we need
 # we look for ocamlfind; if not present, we just don't use it to find
 # libraries
@@ -496,6 +494,10 @@ else
         AC_MSG_CHECKING(Coq version)
         COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
 
+        #Even if the name of the variable is CAMLP4 the value can be camlp5
+        COQCAMLP=$(eval `coqtop -config`; echo ${CAMLP4BIN}${CAMLP4}o)
+        COQCAMLPLIB=$(eval `coqtop -config`; echo ${CAMLP4LIB})
+
         case $COQVERSION in
           8.4*)
 	        enable_coq_support=yes
@@ -730,7 +732,8 @@ AC_SUBST(MENHIR)
 AC_SUBST(enable_profiling)
 AC_SUBST(enable_bin_annot)
 
-AC_SUBST(CAMLP5O)
+AC_SUBST(COQCAMLP)
+AC_SUBST(COQCAMLPLIB)
 
 AC_SUBST(enable_ide)
 AC_SUBST(LABLGTK2LIB)

drivers/alt_ergo.drv

-(* Driver for the most recent version of Alt-Ergo *)
+(* Driver for Alt-Ergo version >= 0.95 *)
 
-import "alt_ergo_bare.drv"
+import "alt_ergo_common.drv"
 
 theory BuiltIn
+
+  (* Alt-Ergo >= 0.95 supports enumerated datatypes and records *)
+
   meta "eliminate_algebraic" "keep_enums"
   meta "eliminate_algebraic" "keep_recs"
+
 end
 
 
 theory int.EuclideanDivision
 
-  (* protection against wrongs semantics for negative arguments *)
+  (* protection against wrong semantics for negative arguments
+    last checked on 0.99.1: this is still needed
+  *)
 
   prelude "logic safe_eucl_div: int, int -> int"
   prelude "axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y"
@@ -25,7 +31,9 @@ end
 
 theory int.ComputerDivision
 
-  (* protection against wrongs semantics for negative arguments *)
+  (* protection against wrong semantics for negative arguments
+     last checked on 0.99.1: this is still needed
+  *)
 
   prelude "logic safe_comp_div: int, int -> int"
   prelude "axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y"
@@ -38,15 +46,6 @@ theory int.ComputerDivision
 
 end
 
-theory map.Map
-  syntax type  map "(%1,%2) farray"
-
-  syntax function get "(%1[%2])"
-  syntax function set "(%1[%2 <- %3])"
-
-  remove prop Select_eq
-  remove prop Select_neq
-end
 
 (*
 Local Variables:

drivers/alt_ergo_0.92.drv

-(* Driver for Alt-Ergo version <= 0.92 *)
-
-import "alt_ergo_bare.drv"
-
-theory BuiltIn
-  meta "printer_option" "no_type_cast"
-end
-
-(*
-Local Variables:
-mode: why
-compile-command: "make -C .. bench"
-End:
-*)

drivers/alt_ergo_0.93.drv

@@ -4,23 +4,13 @@
    - maps
 *)
 
-import "alt_ergo_bare.drv"
+import "alt_ergo_common.drv"
 
 theory BuiltIn
   meta "eliminate_algebraic" "keep_enums"
   meta "printer_option"      "no_type_cast"
 end
 
-theory map.Map
-  syntax type  map "(%1,%2) farray"
-
-  syntax function get "(%1[%2])"
-  syntax function set "(%1[%2 <- %3])"
-
-  remove prop Select_eq
-  remove prop Select_neq
-end
-
 (*
 Local Variables:
 mode: why

drivers/alt_ergo_0.94.drv

@@ -4,10 +4,12 @@
    - Euclidean division
 *)
 
-import "alt_ergo_0.93.drv"
+import "alt_ergo_common.drv"
 
 theory BuiltIn
+  meta "eliminate_algebraic" "keep_enums"
   meta "eliminate_algebraic" "keep_recs"
+  meta "printer_option"      "no_type_cast"
 end
 
 theory int.EuclideanDivision

drivers/alt_ergo_bare.drv → drivers/alt_ergo_common.drv

-(* Why driver for Alt-Ergo *)
+(* Why drivers for Alt-Ergo: common part *)
 
-prelude "(* this is a prelude for Alt-Ergo*)"
+prelude "(* this is the prelude for Alt-Ergo, any versions *)"
 
 printer "alt-ergo"
 filename "%f-%t-%g.why"
@@ -9,7 +9,7 @@ valid "Valid"
 invalid "Invalid"
 unknown "I don't know" ""
 timeout "Timeout"
-timeout "Steps limit reached"
+stepslimitexceeded "Steps limit reached"
 outofmemory "Fatal error: out of memory"
 outofmemory "Fatal error: exception Stack_overflow"
 fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
@@ -167,3 +167,13 @@ theory algebra.AC
   remove prop Comm.Comm
   remove prop Assoc
 end
+
+theory map.Map
+  syntax type  map "(%1,%2) farray"
+
+  syntax function get "(%1[%2])"
+  syntax function set "(%1[%2 <- %3])"
+
+  remove prop Select_eq
+  remove prop Select_neq
+end

drivers/cvc4.drv

-import "cvc4_bare.drv"
+(** Why3 driver for CVC4 <= 1.3 *)
+
+prelude "(set-logic AUFNIRA)"
+(*
+    A  : Array
+    UF : Uninterpreted Function
+    NIRA : NonLinear Integer Reals Arithmetic
+*)
+
+import "smt-libv2.drv"
 import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate"
+transformation "encoding_smt"
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+
+
+(** Extra theories supported by CVC4 *)
+
+(* Disabled:
+   CVC4 division seems to be neither the Euclidean one, nor the Computer one
+
+theory int.EuclideanDivision
+   syntax function div "(div %1 %2)"
+   syntax function mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+
+theory int.ComputerDivision
+   syntax function div "(div %1 %2)"
+   syntax function mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+*)

drivers/metitarski.drv

@@ -222,8 +222,8 @@ theory real.PowerReal
   prelude "include('Axioms/pow.ax')."
 
   (* These follow from Metitarski's axioms. *)
+  remove prop Pow_def
   remove prop Pow_one_y
-  remove prop Pow_exp_log
 end
 
 (* support for integers disabled because may be inconsistent

drivers/smt-libv2.drv

-(* Why driver for SMT-lib v2 syntax *)
+(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
 
-prelude ";;; this is a prelude for smt-lib v2"
-(*prelude "(set-logic AUFNIRA)"*)
-(** A  : Array
+prelude ";;; generated by SMT-LIB2 driver"
+
+(*
+
+Note: we do not insert any command "set-logic" because its
+interpretation is specific to provers
+
+prelude "(set-logic AUFNIRA)"
+
+    A  : Array
     UF : Uninterpreted Function
     DT : Datatypes (not needed at the end ...)
     NIRA : NonLinear Integer Reals Arithmetic