zarith enabled by default (should be harmless), Jessie3 resurrected, ROADMAP updated

ROADMAP

@@ -109,13 +109,20 @@
 ** support de Yices 2 ? interesserait Cesar
 
 
-==================== Roadmap for release 0.83 ========================
+==================== Roadmap for release 0.90 ========================
 
 == New Features to announce ==
 
-* fixed compilation bug with lablgtk 2.18
+= syntax =
+
 * new clause "diverges"
 * clauses "reads" and "writes" accept an empty set
+* modified syntax for "abstract"
+* TODO: lemmas with parameters
+
+= other =
+
+* fixed compilation bug with lablgtk 2.18
 * improved support for Isabelle
 
 == Final preparation ==
@@ -127,7 +134,7 @@
 * check that nightly bench is OK
 * check that "make xml-validate-local" is OK
   (see below : copy the dtd on the web)
-* put 0.83 in file Version
+* put 0.90 in file Version
 * check/update the content of the About dialog in src/ide/gconfig.ml
   around lines 550-600
 * check headers
@@ -136,34 +143,34 @@
     in ./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.83.tar.gz
+* test distrib/why3-0.90.tar.gz
 * install web page for why2 which includes an updated page for the
   quick migration guide. (sources are in CVS repository
   ~filliatr/ARCHIVE/www/why)
 * put on the web page
- - why3-0.83.tar.gz
-   cp distrib/why3-0.83.tar.gz /users/www-perso/projets/why3/download
+ - why3-0.90.tar.gz
+   cp distrib/why3-0.90.tar.gz /users/www-perso/projets/why3/download
 
  - the manual in PDF
-   cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.83.pdf
+   cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.90.pdf
 
  - the HTML version of the manual (content of doc/html)
-   cp -r doc/html /users/www-perso/projets/why3/doc-0.83
+   cp -r doc/html /users/www-perso/projets/why3/doc-0.90
 
  - why3session.dtd
    cp 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.83
+   cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.90
    rm /users/www-perso/projets/why3/stdlib
-   ln -s /users/www-perso/projets/why3/stdlib-0.83 \
+   ln -s /users/www-perso/projets/why3/stdlib-0.90 \
             /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.83
+    cp -r doc/apidoc /users/www-perso/projets/why3/api-0.90
     rm /users/www-perso/projets/why3/api
-    ln -s /users/www-perso/projets/why3/api-0.83 \
+    ln -s /users/www-perso/projets/why3/api-0.90 \
       /users/www-perso/projets/why3/api
    (PROBLEME avec style.css ? Ou est le probleme ?)
  - update the main HTML page (sources are in repository why3-www)
@@ -178,9 +185,9 @@
    chmod -R g+w /users/www-perso/projets/why3
 
 * make a last commit:
- - git commit -m "release 0.83"
- - add tag 0.83 to the git repository, using
-   git tag 0.83
+ - git commit -m "release 0.90"
+ - add tag 0.90 to the git repository, using
+   git tag 0.90
  - do not forget to push it using
    git push
    git push --tags

configure.in

@@ -73,8 +73,7 @@ AC_ARG_ENABLE(native-code,
 
 AC_ARG_ENABLE(zarith,
     [  --enable-zarith         use extra arbitrary-precision lib Zarith],,
-    [enable_zarith=no
-     reason_zarith=" (disabled by default)"])
+    enable_zarith=yes)
 
 
 # IDE
@@ -645,11 +644,10 @@ if test "$enable_frama_c" = yes ; then
       FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|Version: *\(.*\)$|\1|p'`
       AC_MSG_RESULT($FRAMAC_VERSION)
       case $FRAMAC_VERSION in
-         Fluorine-20130501) ;;
-         Fluorine-20130401) ;;
-         *) AC_MSG_WARN(Version Fluorine-20130(4|5)01 required.)
+         Neon-*) ;;
+         *) AC_MSG_WARN(Version Neon required.)
             enable_frama_c=no
-            reason_frama_c=" (version Fluorine required)"
+            reason_frama_c=" (version Neon required)"
             ;;
       esac
       FRAMAC_SHARE=`$FRAMAC -print-path`

modules/mach/int.mlw

@@ -75,7 +75,7 @@ module Bounded_int
     requires { "expl:integer overflow" in_bounds (to_int a - to_int b) }
     ensures  { to_int result = to_int a - to_int b }
 
-  val (*) (a:t) (b:t) : t
+  val ( *) (a:t) (b:t) : t
     requires { "expl:integer overflow" in_bounds (to_int a * to_int b) }
     ensures  { to_int result = to_int a * to_int b }
 
@@ -83,6 +83,12 @@ module Bounded_int
     requires { "expl:integer overflow" in_bounds (- (to_int a)) }
     ensures  { to_int result = - (to_int a) }
 
+  val eq (a:t) (b:t) : bool
+    ensures { result = True <-> to_int a = to_int b }
+
+  val ne (a:t) (b:t) : bool
+    ensures { result = True <-> to_int a <> to_int b }
+
   axiom extensionality: forall x y: t. to_int x = to_int y -> x = y
 
   val (<=) (a:t) (b:t) : bool

src/jessie/ACSLtoWhy3.ml

@@ -52,22 +52,42 @@ open Why3
 let env,config =
   try
     (* reads the Why3 config file *)
+    Self.result "Loading Why3 configuration...";
     let config : Whyconf.config = Whyconf.read_config None in
     (* the [main] section of the config file *)
     let main : Whyconf.main = Whyconf.get_main config in
     let env : Env.env = Env.create_env (Whyconf.loadpath main) in
+    Self.result "Why3 environment loaded.";
     env,config
   with e ->
-    Self.fatal "Exception raised in Why3 env:@ %a" Exn_printer.exn_printer e
+    Self.fatal "Exception raised while reading Why3 environment:@ %a"
+      Exn_printer.exn_printer e
 
-let find th s = Theory.ns_find_ls th.Theory.th_export [s]
-let find_type th s = Theory.ns_find_ts th.Theory.th_export [s]
+let find th s =
+  try
+    Theory.ns_find_ls th.Theory.th_export [s]
+  with e ->
+    Self.fatal "Exception raised while loading Why3 symbol %s:@ %a"
+      s Exn_printer.exn_printer e
 
-(* let () = Self.result "Loading Why3 theories" *)
+let find_type th s =
+  try
+    Theory.ns_find_ts th.Theory.th_export [s]
+  with e ->
+    Self.fatal "Exception raised while loading Why3 type %s:@ %a"
+      s Exn_printer.exn_printer e
+
+let () = Self.result "Loading Why3 theories..."
 
 (* int.Int theory *)
 let int_type : Ty.ty = Ty.ty_int
-let int_theory : Theory.theory = Env.find_theory env ["int"] "Int"
+let int_theory : Theory.theory =
+  try
+    Env.find_theory env ["int"] "Int"
+  with e ->
+    Self.fatal "Exception raised while loading int theory:@ %a"
+      Exn_printer.exn_printer e
+
 let add_int : Term.lsymbol = find int_theory "infix +"
 let sub_int : Term.lsymbol = find int_theory "infix -"
 let minus_int : Term.lsymbol = find int_theory "prefix -"
@@ -97,104 +117,107 @@ let map_ts : Ty.tysymbol = find_type map_theory "map"
 let map_get : Term.lsymbol = find map_theory "get"
 
 
+let () = Self.result "Loading Why3 modules..."
+
+let find_ps mo s =
+  try
+    Mlw_module.ns_find_ps mo.Mlw_module.mod_export [s]
+  with e ->
+    Self.fatal "Exception raised while loading Why3 program symbol %s:@ %a"
+      s Exn_printer.exn_printer e
+
+let find_ls mo s = find mo.Mlw_module.mod_theory s
+
 (* ref.Ref module *)
 
 let ref_modules, ref_theories =
-  Env.read_lib_file (Mlw_main.library_of_env env) ["ref"]
+  try
+    Env.read_lib_file (Mlw_main.library_of_env env) ["ref"]
+  with e ->
+    Self.fatal "Exception raised while loading ref module:@ %a"
+      Exn_printer.exn_printer e
 
 let ref_module : Mlw_module.modul = Stdlib.Mstr.find "Ref" ref_modules
 
 let ref_type : Mlw_ty.T.itysymbol =
   Mlw_module.ns_find_its ref_module.Mlw_module.mod_export ["ref"]
 
-let ref_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["ref"]
+let ref_fun : Mlw_expr.psymbol = find_ps ref_module "ref"
 
-let get_logic_fun : Term.lsymbol =
-  find ref_module.Mlw_module.mod_theory "prefix !"
+let get_logic_fun : Term.lsymbol = find_ls ref_module "prefix !"
 
-let get_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["prefix !"]
+let get_fun : Mlw_expr.psymbol = find_ps ref_module "prefix !"
 
-let set_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["infix :="]
+let set_fun : Mlw_expr.psymbol = find_ps ref_module "infix :="
 
 (* mach_int.Int32 module *)
 
 let mach_int_modules, _mach_int_theories =
-  Env.read_lib_file (Mlw_main.library_of_env env) ["mach_int"]
+  try
+    Env.read_lib_file (Mlw_main.library_of_env env) ["mach";"int"]
+  with e ->
+    Self.fatal "Exception raised while loading mach.int modules:@ %a"
+      Exn_printer.exn_printer e
 
-let int32_module : Mlw_module.modul = Stdlib.Mstr.find "Int32" mach_int_modules
+let int32_module : Mlw_module.modul =
+  try
+    Self.result "Looking up module mach.int.Int32";
+    Stdlib.Mstr.find "Int32" mach_int_modules
+  with Not_found ->
+    Self.fatal "Module mach.int.Int32 not found"
 
 let int32_type : Why3.Ty.tysymbol =
   Mlw_module.ns_find_ts int32_module.Mlw_module.mod_export ["int32"]
 
-let int32_to_int : Term.lsymbol =
-  find int32_module.Mlw_module.mod_theory "to_int"
+let int32_to_int : Term.lsymbol = find_ls int32_module "to_int"
 
-let add32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["add"]
+let add32_fun : Mlw_expr.psymbol = find_ps int32_module "infix +"
 
-let sub32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["sub"]
+let sub32_fun : Mlw_expr.psymbol = find_ps int32_module "infix -"
 
-let mul32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["mul"]
+let mul32_fun : Mlw_expr.psymbol = find_ps int32_module "infix *"
 
-let neg32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["neg"]
+let neg32_fun : Mlw_expr.psymbol = find_ps int32_module "prefix -"
 
-let eq32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["eq"]
+let eq32_fun : Mlw_expr.psymbol = find_ps int32_module "eq"
 
-let ne32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["ne"]
+let ne32_fun : Mlw_expr.psymbol = find_ps int32_module "ne"
 
-let le32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["le"]
+let le32_fun : Mlw_expr.psymbol = find_ps int32_module "infix <="
 
-let lt32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["lt"]
+let lt32_fun : Mlw_expr.psymbol = find_ps int32_module "infix <"
 
-let ge32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["ge"]
+let ge32_fun : Mlw_expr.psymbol = find_ps int32_module "infix >="
 
-let gt32_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["gt"]
+let gt32_fun : Mlw_expr.psymbol = find_ps int32_module "infix >"
 
-let int32ofint_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["of_int"]
+let int32ofint_fun : Mlw_expr.psymbol = find_ps int32_module "of_int"
 
 (* mach_int.Int64 module *)
 
-let mach_int_modules, mach_int_theories =
-  Env.read_lib_file (Mlw_main.library_of_env env) ["mach_int"]
-
-let int64_module : Mlw_module.modul = Stdlib.Mstr.find "Int64" mach_int_modules
+let int64_module : Mlw_module.modul =
+  try
+    Self.result "Looking up module mach.int.Int64";
+    Stdlib.Mstr.find "Int64" mach_int_modules
+  with Not_found ->
+    Self.fatal "Module mach.int.Int64 not found"
 
 let int64_type : Why3.Ty.tysymbol =
   Mlw_module.ns_find_ts int64_module.Mlw_module.mod_export ["int64"]
 
-let int64_to_int : Term.lsymbol =
-  find int64_module.Mlw_module.mod_theory "to_int"
+let int64_to_int : Term.lsymbol = find_ls int64_module "to_int"
 
-let add64_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["add"]
+let add64_fun : Mlw_expr.psymbol = find_ps int64_module "infix +"
 
-let sub64_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["sub"]
+let sub64_fun : Mlw_expr.psymbol = find_ps int64_module "infix -"
 
-let mul64_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["mul"]
+let mul64_fun : Mlw_expr.psymbol = find_ps int64_module "infix *"
 
-let le64_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["le"]
+let le64_fun : Mlw_expr.psymbol = find_ps int64_module "infix <="
 
-let lt64_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["lt"]
+let lt64_fun : Mlw_expr.psymbol = find_ps int64_module "infix <"
 
-let int64ofint_fun : Mlw_expr.psymbol =
-  Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["of_int"]
+let int64ofint_fun : Mlw_expr.psymbol = find_ps int64_module "of_int"
 
 (* array.Array module *)
 
@@ -477,7 +500,7 @@ let coerce_to_int ty t =
     | Ctype(TInt(IInt,_attr)) -> t_app int32_to_int [t]
     | Ctype(TInt(ILong,_attr)) -> t_app int64_to_int [t]
     | _ -> Self.not_yet_implemented "coerce_to_int"
-      
+
 
 let rec term_node ~label t =
   match t with
@@ -615,7 +638,7 @@ and tlval ~label (host,offset) =
 
 let eq op ty1 t1 ty2 t2 =
   match ty1,ty2 with
-    | ty1, ty2 when is_int_type ty1 && is_int_type ty2 -> 
+    | ty1, ty2 when is_int_type ty1 && is_int_type ty2 ->
       op (coerce_to_int ty1 t1) (coerce_to_int ty2 t2)
     | Lreal, Lreal -> op t1 t2
     | Ctype _,_ ->
@@ -630,7 +653,7 @@ let eq op ty1 t1 ty2 t2 =
 
 let compare op ty1 t1 ty2 t2 =
   match ty1,ty2 with
-    | ty1,ty2 when is_int_type ty1 && is_int_type ty2 -> 
+    | ty1,ty2 when is_int_type ty1 && is_int_type ty2 ->
       t_app op [coerce_to_int ty1 t1;coerce_to_int ty2 t2]
     | Lreal, Lreal -> assert false
     | Ctype _,_ ->
@@ -681,10 +704,10 @@ let rec predicate ~label p =
       Self.not_yet_implemented "predicate Pnot"
     | Pat (_, _) ->
       Self.not_yet_implemented "predicate Pat"
-    | Pseparated _ 
-    | Por (_, _) 
+    | Pseparated _
+    | Por (_, _)
     | Pxor (_, _)
-    | Piff (_, _) 
+    | Piff (_, _)
     | Pif (_, _, _)
     | Plet (_, _)
     | Pexists (_, _)
@@ -984,9 +1007,9 @@ and lval (host,offset) =
     | Mem({enode = BinOp((PlusPI|IndexPI),e,i,ty)}), NoOffset ->
       (* e[i] -> Map.get e i *)
       let e = expr e in
-      let ity = 
+      let ity =
         match ty with
-          | TPtr(t,_) -> ctype t 
+          | TPtr(t,_) -> ctype t
           | _ -> assert false
       in
       let i = expr i in
@@ -1042,7 +1065,7 @@ let instr i =
     let e = functional_expr e in
     let e = Mlw_expr.e_app e (List.map expr el) in
     assignment lv e loc
-  | Asm (_, _, _, _, _, _) ->
+  | Asm _ ->
     Self.not_yet_implemented "instr Asm"
   | Skip _loc ->
     Mlw_expr.e_void

src/jessie/register.ml

@@ -54,19 +54,33 @@ let get_prover config env acc (short, name) =
 
 let process () =
   let prog = Ast.get () in
-  (* File.pretty_ast (); *)
+  (* File.pretty_ast ();  *)
   let provers =
-    List.fold_left
-      (get_prover ACSLtoWhy3.config ACSLtoWhy3.env)
-      []
-      [ "Z431", "Z3,4.3.1";
-        "Z32 ", "Z3,3.2";
-        "C241", "CVC3,2.4.1";
-        "A951", "Alt-Ergo,0.95.1,";
+    try
+      ACSLtoWhy3.Self.result "Loading prover drivers...";
+      List.fold_left
+        (get_prover ACSLtoWhy3.config ACSLtoWhy3.env)
+        []
+        [ "Z431", "Z3,4.3.1";
+          "Z32 ", "Z3,3.2";
+          "C241", "CVC3,2.4.1";
+          "C413", "CVC4,1.3";
+          "A952", "Alt-Ergo,0.95.2,";
         ]
+    with e ->
+      ACSLtoWhy3.Self.fatal "Exception raised when loading prover drivers:@ %a"
+        Exn_printer.exn_printer e
+  in
+  let theories =
+    try
+      ACSLtoWhy3.Self.result "Translating to Why3...";
+      ACSLtoWhy3.prog prog
+    with e ->
+      ACSLtoWhy3.Self.fatal "Exception raised when loading prover drivers:@ %a"
+        Exn_printer.exn_printer e
   in
-  let theories = ACSLtoWhy3.prog prog in
   try
+    ACSLtoWhy3.Self.result "Running provers...";
     List.iter (fun th ->
       ACSLtoWhy3.Self.result "running theory 1:";
       ACSLtoWhy3.Self.result "@[<hov 2>%a@]" Pretty.print_theory th;
@@ -87,7 +101,8 @@ let process () =
       in ())
     theories
   with e ->
-    ACSLtoWhy3.Self.fatal "Exception raised when running provers:@ %a" Exn_printer.exn_printer e
+    ACSLtoWhy3.Self.fatal "Exception raised when running provers:@ %a"
+      Exn_printer.exn_printer e
 
 
 let (_unused : (unit -> unit) -> unit -> unit) =
@@ -98,4 +113,9 @@ let (_unused : (unit -> unit) -> unit -> unit) =
     (Datatype.func Datatype.unit Datatype.unit)
 
 let run () =  if ACSLtoWhy3.Enabled.get () then process ()
-let () = Db.Main.extend run
+let () =
+  try
+    Db.Main.extend run
+  with e ->
+    ACSLtoWhy3.Self.fatal "Exception raised when loading Jessie3:@ %a"
+      Exn_printer.exn_printer e