Merge branch 'master' into new_system

.gitattributes

-/examples/in_progress/ export-ignore
-/examples/hoare_logic/draft/ export-ignore
-/tests/ export-ignore
-/bench/encoding/ export-ignore
-/misc/ export-ignore
-/ROADMAP export-ignore
-/DEVELOPER.readme export-ignore
-/opam/ export-ignore
-.gitignore export-ignore
 .gitattributes export-ignore
+.gitignore export-ignore
+.keepme export-ignore
+
+/.gitlab-ci.yml export-ignore
+/.mailmap export-ignore
 /check.sh export-ignore
+/DEVELOPER.readme export-ignore
+/ROADMAP export-ignore
 /TODO export-ignore
+
+/bench/encoding/ export-ignore
+/examples/in_progress/ export-ignore
+/misc/ export-ignore
+/opam/ export-ignore
+/tests/ export-ignore

.mailmap

@@ -9,7 +9,7 @@ Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@evariste.(none
 Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@gemini.(none)>
 Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@balrog.(none)>
 Clément Fumex <clement.fumex@inria.fr> <fumex@moloch.lri.fr>
-Léon Gondelman <gondelmans@lri.fr> <gondelmans@lri.fr>
+Léon Gondelman <gondelmans@lri.fr>
 Léon Gondelman <gondelmans@lri.fr> <lgondelmann@gmail.com>
 Léon Gondelman <gondelmans@lri.fr> <lgondelman@lg-PC.(none)>
 Léon Gondelman <gondelmans@lri.fr> <leon@ubuntu.(none)>
@@ -19,6 +19,7 @@ Claude Marché <claude.marche@inria.fr> <Claude.Marche@inria.fr>
 Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)>
 Claude Marché <claude.marche@inria.fr> <cmarche@orcus.(none)>
 Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)>
+Guillaume Melquiond <guillaume.melquiond@inria.fr>
 Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr>
 Kim Nguyễn <kim.nguyen@lri.fr> <kn@lri.fr>
 Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@lri.fr>
@@ -26,9 +27,9 @@ Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
 Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyenthiminhtuyen@minhtuyen.local>
 Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <thi-minh-tuyen.nguyen@inria.fr>
 Andrei Paskevich <andrei@lri.fr> <andrei@tertium.org>
+Mário Pereira <mpereira@lri.fr>
 Mário Pereira <mpereira@lri.fr> <mario.j.p.pereira@gmail.com>
 Mário Pereira <mpereira@lri.fr> <parreira@lri.fr>
-Mário Pereira <mpereira@lri.fr> <mpereira@lri.fr>
-Asma Tafat-Bouzid <atafat@lri.fr> <atafat@lri.fr>
+Asma Tafat-Bouzid <atafat@lri.fr>
 Asma Tafat-Bouzid <atafat@lri.fr> <atafat@atafat-desktop.(none)>
 Piotr Trojanek <piotr.trojanek@altran.com> <piotr.trojanek@gmail.com>

INSTALL → INSTALL.md

-
-                  Installation instructions
+Installation instructions
+=========================
 
 
 Installation from a source distribution (tarball)
@@ -11,7 +11,7 @@ After unpacking, installation is done by
     make
     make install (as root)
 
-To install also the Ocaml library do
+To install also the Ocaml library, do
 
     make byte
     make install-lib (as root)
@@ -25,12 +25,13 @@ First run
     autoconf
     automake --add-missing
 
-to build the ./configure file and install the helper scripts, then follow
-instructions from the section above.
+to build the `./configure` file and install the helper scripts, then follow
+the instructions from the section above.
 
 
 Detailed instructions
 ---------------------
 
 For detailed instructions and required dependencies, please see
-the manual (doc/manual.pdf), Chapter 5 "Compilation, Installation".
+the manual [doc/manual.pdf](http://why3.lri.fr/manual.pdf), Chapter 5
+[Compilation, Installation](http://why3.lri.fr/doc/install.html).

README → README.md

+WHY3
+====
 
 Why3 is a platform for deductive program verification. It provides
 a rich language for specification and programming, called WhyML, and
@@ -11,42 +13,43 @@ automated extraction mechanism. WhyML is also used as an intermediate
 language for the verification of C, Java, or Ada programs.
 
 PROJECT HOME
-============
+------------
 
-http://why3.lri.fr
+http://why3.lri.fr/
 
-https://gforge.inria.fr/projects/why3
+https://gitlab.inria.fr/why3/why3
 
 DOCUMENTATION
-=============
+-------------
 
-The documentation (a tutorial and a reference manual) is in
-the file doc/manual.pdf.
+The documentation (a tutorial and a reference manual) is in the file
+[doc/manual.pdf](http://why3.lri.fr/manual.pdf) or online at
+http://why3.lri.fr/doc/.
 
-Various examples can be found in the subdirectories theories/
-and examples/.
+Various examples can be found in the subdirectories [theories/](theories)
+and [examples/](examples).
 
 Mailing list (Why3 Club):
   http://lists.gforge.inria.fr/mailman/listinfo/why3-club
 
 Bug Tracking System:
-  https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse
+  https://gitlab.inria.fr/why3/why3/issues
 
 COPYRIGHT
-=========
+---------
 
 This program is distributed under the GNU LGPL 2.1. See the enclosed
-file LICENSE.
+file [LICENSE](LICENSE).
 
-The files src/util/extmap.ml{i} are derived from the sources of
-OCaml 3.12 standard library, and are distributed under the GNU
-LGPL version 2 (see file OCAML-LICENSE).
+The files [src/util/extmap.ml{i}](src/util/extmap.mli) are derived from the
+sources of OCaml 3.12 standard library, and are distributed under the GNU
+LGPL version 2 (see file [OCAML-LICENSE](OCAML-LICENSE)).
 
 Icon sets for the graphical interface of Why3 are subject to specific
 licenses, some of them may forbid commercial usage. These specific
-licenses are detailed in files share/images/*/*.txt
+licenses are detailed in files [share/images/\*/\*.txt](share/images).
 
 INSTALLATION
-============
+------------
 
-See the file INSTALL.
+See the file [INSTALL.md](INSTALL.md).

ROADMAP

@@ -142,9 +142,11 @@
 * upload distrib/why3-0.86.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
 
 * upload the documentation on the web page
+ - cp share/why3session.dtd /users/www-perso/projets/why3/
  - cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.86.pdf
+   ln -s -n -f download/manual-0.86.pdf /users/www-perso/projets/why3/manual.pdf
  - cp -r doc/html /users/www-perso/projets/why3/doc-0.86
- - cp share/why3session.dtd /users/www-perso/projets/why3/
+   ln -s -n -f doc-0.86 /users/www-perso/projets/why3/doc
  - cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.86
    ln -s -n -f stdlib-0.86 /users/www-perso/projets/why3/stdlib
  - cp -r doc/apidoc /users/www-perso/projets/why3/api-0.86

doc/manual.tex

@@ -108,7 +108,7 @@
 %BEGIN LATEX
 \begin{LARGE}
 %END LATEX
-  Version \whyversion{}, October 2017
+  Version \whyversion{}, November 2017
 %BEGIN LATEX
 \end{LARGE}
 %END LATEX

drivers/isabelle-common.gen

@@ -9,7 +9,6 @@ time "why3cpulimit time : %s s"
 transformation "eliminate_epsilon"
 transformation "eliminate_if_fmla"
 transformation "eliminate_let_fmla"
-transformation "eliminate_projections"
 transformation "simplify_formula"
 
 theory BuiltIn

opam/why3-base/opam

@@ -10,9 +10,9 @@ authors: [
 
 homepage: "http://why3.lri.fr/"
 license: "GNU Lesser General Public License version 2.1"
-doc: "http://why3.lri.fr/#documentation"
-bug-reports: "https://gforge.inria.fr/tracker/?func=browse&group_id=2990&atid=10293"
-dev-repo: "https://scm.gforge.inria.fr/anonscm/git/why3/why3.git"
+doc: "http://why3.lri.fr/doc/"
+bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
+dev-repo: "https://gitlab.inria.fr/why3/why3.git"
 
 tags: [
   "deductive"
@@ -46,6 +46,7 @@ build-doc: [
 depends: [
   "ocamlfind"
   "menhir" {>= 20150629}
+  "num"
 ]
 
 depopts: [

opam/why3-base/url

-archive: "https://gforge.inria.fr/frs/download.php/file/37147/why3-0.88.0.tar.gz"
-checksum: "1aef885ff8eee34107585e11db623a8d"

opam/why3/opam

@@ -7,11 +7,13 @@ authors: [
   "Guillaume Melquiond"
   "Andrei Paskevich"
 ]
+
 homepage: "http://why3.lri.fr/"
 license: "GNU Lesser General Public License version 2.1"
-doc: "http://why3.lri.fr/#documentation"
-bug-reports: "https://gforge.inria.fr/tracker/?func=browse&group_id=2990&atid=10293"
-dev-repo: "https://scm.gforge.inria.fr/anonscm/git/why3/why3.git"
+doc: "http://why3.lri.fr/doc/"
+bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
+dev-repo: "https://gitlab.inria.fr/why3/why3.git"
+
 tags: [
   "deductive"
   "program verification"
@@ -21,7 +23,7 @@ tags: [
 ]
 available: [ ocaml-version >= "4.02.3" & ocaml-version < "4.06" ]
 depends: [
-  "why3-base" { = "0.88.0" }
+  "why3-base" { = "0.88.1" }
   "lablgtk"
   "conf-gtksourceview"
   "zarith"

src/coq-tactic/why3tac.ml4

@@ -175,18 +175,18 @@ let get_prover s =
 
 (* Coq constants *)
 
-let coq_ref_BinInt = coq_reference "Why3" ["ZArith"; "BinInt"]
-let coq_Z = coq_ref_BinInt "Z"
-let coq_Zplus = coq_ref_BinInt "Zplus"
-let coq_Zmult = coq_ref_BinInt "Zmult"
-let coq_Zopp = coq_ref_BinInt "Zopp"
-let coq_Zminus = coq_ref_BinInt "Zminus"
-let coq_Zdiv = coq_reference "Why3" ["ZArith"; "Zdiv"] "Zdiv"
-let coq_Zgt = coq_ref_BinInt "Zgt"
-let coq_Zle = coq_ref_BinInt "Zle"
-let coq_Zge = coq_ref_BinInt "Zge"
-let coq_Zlt = coq_ref_BinInt "Zlt"
+let coq_ref_BinInt = coq_reference "Why3" ["ZArith"; "BinInt"; "Z"]
+let coq_Zplus = coq_ref_BinInt "add"
+let coq_Zmult = coq_ref_BinInt "mul"
+let coq_Zopp = coq_ref_BinInt "opp"
+let coq_Zminus = coq_ref_BinInt "sub"
+let coq_Zdiv = coq_ref_BinInt "div"
+let coq_Zgt = coq_ref_BinInt "gt"
+let coq_Zle = coq_ref_BinInt "le"
+let coq_Zge = coq_ref_BinInt "ge"
+let coq_Zlt = coq_ref_BinInt "lt"
 let coq_ref_BinNums = coq_reference "Why3" ["Numbers"; "BinNums"]
+let coq_Z = coq_ref_BinNums "Z"
 let coq_Z0 = coq_ref_BinNums "Z0"
 let coq_Zpos = coq_ref_BinNums "Zpos"
 let coq_Zneg = coq_ref_BinNums "Zneg"
@@ -209,6 +209,11 @@ let coq_Rinv = coq_ref_Rdefinitions "Rinv"
 let coq_Rminus = coq_ref_Rdefinitions "Rminus"
 let coq_Rdiv = coq_ref_Rdefinitions "Rdiv"
 let coq_powerRZ = coq_reference "Why3" ["Reals"; "Rfunctions"] "powerRZ"
+IFDEF COQ87 THEN
+let coq_IZR = coq_ref_Rdefinitions "IZR"
+ELSE
+let coq_IZR = coq_reference "Why3" ["Reals"; "Raxioms"] "IZR"
+END
 
 let coq_Logic = coq_reference "Why3" ["Init"; "Logic"]
 let coq_False = coq_Logic "False"
@@ -480,13 +485,35 @@ let const_of_big_int is_neg b =
          ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) }))
     ty_int
 
+let const_of_big_int_real is_neg b =
+  let s = Big_int.string_of_big_int b in
+  Term.t_const
+    (Number.(ConstReal { rc_negative = is_neg ;
+                         rc_abs = real_const_dec s "0" None}))
+    ty_real
+
 (* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
+let rec tr_arith_constant_IZR evd dep t = match kind evd t with
+  | Construct _ when is_global evd coq_Z0 t ->
+    Term.t_const (Number.(ConstReal { rc_negative = false ;
+      rc_abs = real_const_dec "0" "0" None })) ty_real
+  | App (f, [|a|]) when is_global evd coq_Zpos f ->
+    const_of_big_int_real false (tr_positive evd a)
+  | App (f, [|a|]) when is_global evd coq_Zneg f ->
+    const_of_big_int_real true (tr_positive evd a)
+  | Cast (t, _, _) ->
+    tr_arith_constant_IZR evd dep t
+  | _ ->
+    raise NotArithConstant
+
 let rec tr_arith_constant evd dep t = match kind evd t with
   | Construct _ when is_global evd coq_Z0 t -> Term.t_nat_const 0
   | App (f, [|a|]) when is_global evd coq_Zpos f ->
       const_of_big_int false (tr_positive evd a)
   | App (f, [|a|]) when is_global evd coq_Zneg f ->
       const_of_big_int true (tr_positive evd a)
+  | App (f, [|a|]) when is_global evd coq_IZR f ->
+      tr_arith_constant_IZR evd dep a
   | Const _ when is_global evd coq_R0 t ->
       Term.t_const (Number.(ConstReal { rc_negative = false ;
         rc_abs = real_const_dec "0" "0" None }))

src/driver/call_provers.ml

@@ -392,7 +392,7 @@ type prover_update =
 
 let result_buffer : (server_id, prover_update) Hashtbl.t = Hashtbl.create 17
 
-let get_new_results ~blocking = (* TODO: handle ProverStarted events *)
+let fetch_new_results ~blocking = (* TODO: handle ProverStarted events *)
   List.iter (fun (id, r) ->
     let x = match r with
     | Some r -> ProverFinished r
@@ -400,21 +400,21 @@ let get_new_results ~blocking = (* TODO: handle ProverStarted events *)
     Hashtbl.add result_buffer id x)
     (wait_for_server_result ~blocking)
 
-let query_result_buffer id =
-  try let r = Hashtbl.find result_buffer id in
-      Hashtbl.remove result_buffer id; r
-  with Not_found -> NoUpdates
-
-let forward_results ~blocking =
-  get_new_results ~blocking;
-  let q = Queue.create () in
+let get_new_results ~blocking =
+  fetch_new_results ~blocking;
+  let q = ref [] in
   Hashtbl.iter (fun key element ->
     if element = ProverStarted && blocking then
       ()
     else
-      Queue.push (ServerCall key, element) q) result_buffer;
+      q := (ServerCall key, element) :: !q) result_buffer;
   Hashtbl.clear result_buffer;
-  q
+  !q
+
+let query_result_buffer id =
+  try let r = Hashtbl.find result_buffer id in
+      Hashtbl.remove result_buffer id; r
+  with Not_found -> NoUpdates
 
 let editor_result ret = {
   pr_answer = Unknown ("", None);
@@ -427,7 +427,7 @@ let editor_result ret = {
 
 let query_call = function
   | ServerCall id ->
-      get_new_results ~blocking:false;
+      fetch_new_results ~blocking:false;
       query_result_buffer id
   | EditorCall pid ->
       let pid, ret = Unix.waitpid [Unix.WNOHANG] pid in
@@ -439,7 +439,7 @@ let rec wait_on_call = function
       begin match query_result_buffer id with
         | ProverFinished r -> r
 	| _ ->
-            get_new_results ~blocking:true;
+            fetch_new_results ~blocking:true;
             wait_on_call pc
       end
   | EditorCall pid ->

src/driver/call_provers.mli

@@ -172,10 +172,8 @@ type prover_update =
   | ProverStarted
   | ProverFinished of prover_result
 
-
-val forward_results: blocking:bool -> (prover_call * prover_update) Queue.t
-(** returns new results that are given by why3server. *)
-
+val get_new_results: blocking:bool -> (prover_call * prover_update) list
+(** returns new results from why3server, in an unordered fashion. *)
 
 val query_call : prover_call -> prover_update
 (** non-blocking function that reports any new updates

src/printer/isabelle.ml

@@ -301,8 +301,10 @@ let rec dest_forall vl t = match t.t_node with
 
 (** Declarations *)
 
-let print_constr info fmt (cs, _) =
-  elems "constr" (print_ls info) (print_ty info) fmt (cs, cs.ls_args)
+let print_constr info fmt (cs, pjl) =
+  elems "constr" (print_ls info)
+    (elem "carg" (print_option (print_ls info)) (print_ty info)) fmt
+    (cs, List.combine pjl cs.ls_args)
 
 let print_tparams = elems' "params" (empty_elem "param" (attrib "name" print_tv))
 

src/session/controller_itp.ml

@@ -376,20 +376,11 @@ let timeout_handler () =
   (* When no tasks are there, probably no tasks were scheduled and the server
      was not launched so getting results could fail. *)
   if Hashtbl.length prover_tasks_in_progress != 0 then begin
-    let results = Call_provers.forward_results ~blocking:S.blocking in
-    while not (Queue.is_empty results) do
-      let (call, prover_update) = Queue.pop results in
-      let c = try Some (Hashtbl.find prover_tasks_in_progress call)
-        with Not_found -> None in
-      match c with
-      | None -> () (* we do nothing. We probably received ProverStarted after
-                      ProverFinished because what is sent to and received from
-                      the server is not ordered. *)
-      | Some c ->
-      begin
-        let (ses,id,pr,callback,started,call,ores) = c in
-
-        match prover_update with
+    let results = Call_provers.get_new_results ~blocking:S.blocking in
+    List.iter (fun (call, prover_update) ->
+      match Hashtbl.find prover_tasks_in_progress call with
+      | (ses,id,pr,callback,started,call,ores) ->
+        begin match prover_update with
         | Call_provers.NoUpdates -> ()
         | Call_provers.ProverStarted ->
             assert (not started);
@@ -414,7 +405,11 @@ let timeout_handler () =
             (* inform the callback *)
             callback (InternalFailure (exn))
         end
-    done
+      | exception Not_found -> ()
+        (* We probably received ProverStarted after ProverFinished,
+           because what is sent to and received from the server is
+           not ordered. *)
+    ) results;
   end;
 
   (* When blocking is activated, we are in script mode and we don't want editors

src/whyml/mlw_decl.ml

@@ -161,7 +161,12 @@ let check_vars vars =
       (Stv.choose vars.vars_tv).tv_name.id_string
 
 let letvar_news = function
-  | LetV pv -> check_vars pv.pv_ity.ity_vars; Sid.singleton pv.pv_vs.vs_name
+  | LetV pv ->
+    check_vars pv.pv_ity.ity_vars;
+    Sreg.fold
+      (fun r acc -> Sid.add r.reg_name acc)
+      pv.pv_ity.ity_vars.vars_reg
+      (Sid.singleton pv.pv_vs.vs_name)
   | LetA ps -> check_vars ps.ps_vars; Sid.singleton ps.ps_name
 
 let ids_of_pvset s pvs =

src/whyml/mlw_module.ml

@@ -615,7 +615,8 @@ let clone_export uc m minst inst =
           let id = id_clone ps.ps_name in
           let aty = conv_aty !mvs ps.ps_aty in
           let vari = Spv.fold (fun pv l ->
-            (t_var (Mvs.find pv.pv_vs !mvs), None)::l) ps.ps_pvset [] in
+            (t_var (Mvs.find_def pv.pv_vs pv.pv_vs !mvs), None)::l)
+            ps.ps_pvset [] in
           (* we save all external pvsymbols to preserve the effects *)
           let spec = { aty.aty_spec with c_variant = vari } in
           let aty = vty_arrow ~spec aty.aty_args aty.aty_result in

tests/python/dicho.py

@@ -3,17 +3,13 @@ from random import randint
 
 n = 42
 a = [0] * n
+#@ assert len(a) == n
 
 a[0] = randint(0, 100)
-i = 1
-while i < n:
-    #@ invariant 1 <= i
+for i in range(1, n):
     #@ invariant forall i1, i2. 0 <= i1 <= i2 < i -> a[i1] <= a[i2]
-    #@ variant   n-i
     a[i] = a[i-1] + randint(0, 10)
-    i = i + 1
 
-#@ assert len(a) == n
 #@ assert forall i1, i2. 0 <= i1 <= i2 < len(a) -> a[i1] <= a[i2]
 
 print(a)

tests/python/mult.py

@@ -15,12 +15,14 @@ if q < 0:
 
 r = 0
 while q > 0:
-    #@ invariant 0 <= q and r + p * q == a * b
+    #@ invariant 0 <= q
+    #@ invariant r + p * q == a * b
     #@ variant   q
+    print(p, q, r)
     if q % 2 == 1:
         r = r + p
     p = p + p
     q = q // 2
-
+print(p, q, r)
 print("a * b =", r)
 #@ assert r == a * b

tests/python/triangular.py

@@ -7,7 +7,7 @@ n = int(input("entrez n : "))
 s = 0
 k = 0
 while k <= n:
-    #@ invariant 0 <= k <= n+1
+    #@ invariant k <= n+1
     #@ invariant s == (k - 1) * k // 2
     #@ variant n - k
     s = s + k