Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 10f84ad8 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Merge branch 'master' into mp

Conflicts:
	Makefile.in
	examples/in_progress/mp2.mlw
parents 20a8de67 e93941ce
:x: marks a potential source of incompatibility
Version 0.88.2, December 7, 2017
--------------------------------
Bug fixes
* `why3 session html`: improved compliance of generated files
* `why3 doc`: fixed missing anchors for operator definitions
* improved build process when `coqtop.byte` is missing
Version 0.88.1, November 6, 2017
--------------------------------
......@@ -8,7 +16,7 @@ API
Provers
* improved support for Isabelle 2017
* fixed support for Coq 8.7
* fixed support for Coq 8.7 (released Oct 17, 2017)
Miscellaneous
* fixed compilation for OCaml 4.06
......@@ -34,16 +42,16 @@ Standard library
compliant to IEEE-754, mapped to SMT-LIB FP theory.
User features
* proof strategies: why3 config now generates default proof strategies
* proof strategies: `why3 config` now generates default proof strategies
using the installed provers. These are available under name "Auto
level 0", "Auto level 1" and "Auto level 2" in why3 ide.
level 0", "Auto level 1" and "Auto level 2" in `why3 ide`.
More details in the manual, section 10.6 "Proof Strategies".
* counterexamples: better support for array values, support for
floating-point values, support for Z3 in addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples".
Provers
* support for Isabelle 2017
* support for Isabelle 2017 (released Oct 2017)
* discarded support for Isabelle 2016 (2016-1 still supported) :x:
* support for Coq 8.6.1 (released Jul 25, 2017)
* tentative support for Coq 8.7
......@@ -89,7 +97,7 @@ Language
Tools
* added a command-line option `--extra-expl-prefix` to specify
additional possible prefixes for VC explanations. Available for
why3 commands `prove` and `ide`.
`why3` commands `prove` and `ide`.
* removed `jstree` style from the `session` command :x:
Transformations
......@@ -158,7 +166,7 @@ Provers
* support for Gappa 1.2 (released May 19, 2015)
Bug fixes
* why3doc: garbled output
* `why3doc`: garbled output
Version 0.86, May 11, 2015
--------------------------
......
This diff is collapsed.
......@@ -121,7 +121,7 @@
* 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
* check the file CHANGES.md, add the release date
* generate documentation
- update the date in doc/manual.tex (near \whyversion{})
......@@ -158,9 +158,6 @@
- make (to check validity)
- make export
* add a new version to the bugtracker:
https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
* The next commit : add +git to the version in file Version
* prepare the OPAM package
......
......@@ -665,15 +665,19 @@ fi
# Isabelle
# Default version used for generation of realization in the case Isabelle is not
# detected or Why3 is compiled with disable-isabelle.
ISABELLEVERSION=2017
if test "$enable_isabelle_libs" = no; then
enable_isabelle_support=no
reason_isabelle_support=" (disabled by user)"
else
AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
if test "$ISABELLE" = no ; then
enable_isabelle_support=no
AC_MSG_WARN(Cannot find isabelle.)
reason_isabelle_support=" (isabelle not found)"
enable_isabelle_support=no
AC_MSG_WARN(Cannot find isabelle.)
reason_isabelle_support=" (isabelle not found)"
else
AC_MSG_CHECKING(Isabelle version)
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, November 2017
Version \whyversion{}, December 2017
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
......@@ -2,11 +2,11 @@
prelude "(set-logic AUFBVDTNIRA)"
(*
A : Array
UF : Uninterpreted Function
BV : BitVectors
DT : Datatypes
NIRA : NonLinear Integer Reals Arithmetic
A : Array
UF : Uninterpreted Function
BV : BitVectors
DT : Datatypes
NIRA : NonLinear Integer Real Arithmetic
*)
(* prelude "(set-logic ALL_SUPPORTED)"
does not seem to include DT
......@@ -14,6 +14,7 @@ prelude "(set-logic AUFBVDTNIRA)"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "discrimination.gen"
transformation "inline_trivial"
......@@ -62,5 +63,3 @@ theory int.EuclideanDivision
remove prop Div_1
end
*)
import "cvc4_bv.gen"
......@@ -17,6 +17,7 @@ model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "discrimination.gen"
transformation "inline_trivial"
......@@ -72,5 +73,3 @@ theory int.ComputerDivision
remove prop Div_1
end
*)
import "cvc4_bv.gen"
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_int *)
theory bv.BV_Gen
syntax function to_uint "(bv2nat %1)"
end
theory bv.BV64
syntax converter of_int "(_ bv%1 64)"
syntax function t'int "(bv2nat %1)"
......
......@@ -205,12 +205,14 @@ module mach.int.Int
end
module mach.int.Int63
syntax val of_int "Z.to_int %1"
syntax converter of_int "%1"
syntax type int63 "int"
syntax function to_int "Z.of_int %1"
syntax literal int63 "%1"
syntax converter of_int "%1"
syntax val of_int "Z.to_int %1"
syntax function to_int "Z.of_int %1"
syntax type int63 "int"
syntax constant min_int63 "Z.of_int min_int"
syntax constant max_int63 "Z.of_int max_int"
syntax constant min_int "min_int"
......@@ -223,8 +225,6 @@ module mach.int.Int63
syntax val ( * ) "%1 * %2"
syntax val ( / ) "%1 / %2"
syntax val ( % ) "%1 mod %2"
syntax val eq "%1 = %2"
syntax val ne "%1 <> %2"
syntax val (=) "%1 = %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
......
......@@ -3,35 +3,25 @@
prelude ";;; SMT-LIB2 driver: bit-vectors, common part"
theory bv.BV_Gen
remove prop size_pos
remove prop nth_out_of_bound
remove prop Nth_zeros
remove prop Nth_ones
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax predicate (==) "(= %1 %2)"
(* Warning: we should NOT remove all the axioms using "allprops" *)
remove prop size_pos
remove prop nth_out_of_bound
remove prop Nth_zeros
remove prop Nth_ones
remove prop two_power_size_val
remove prop max_int_val
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_or
remove prop Nth_bw_xor
remove prop Nth_bw_not
(** Shift operators *)
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop lsr_zeros
......@@ -44,37 +34,84 @@ theory bv.BV_Gen
remove prop Nth_rotate_left
remove prop Nth_rotate_right
(* Conversions from/to integers *)
remove prop two_power_size_val
remove prop max_int_val
(* function to_int - solver specific *)
(* function to_uint - solver specific *)
(* function of_int - solver specific *)
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_int_extensionality
remove prop to_uint_bounds
(*remove prop to_uint_of_int*)
remove prop to_uint_size_bv
remove prop to_uint_zeros
remove prop to_uint_ones
remove prop to_uint_one
(* comparison operators *)
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
(** Arithmetic operators *)
syntax function add "(bvadd %1 %2)"
remove prop to_uint_add
remove prop to_uint_add_bounded
syntax function sub "(bvsub %1 %2)"
remove prop to_uint_sub
remove prop to_uint_sub_bounded
syntax function neg "(bvneg %1)"
remove prop to_uint_neg
syntax function mul "(bvmul %1 %2)"
remove prop to_uint_mul
remove prop to_uint_mul_bounded
syntax function udiv "(bvudiv %1 %2)"
remove prop to_uint_udiv
syntax function urem "(bvurem %1 %2)"
remove prop to_uint_urem
(** Bitvector alternatives for shifts, rotations and nth *)
syntax function lsr_bv "(bvlshr %1 %2)"
(* remove prop lsr_bv_is_lsr *)
remove prop to_uint_lsr
syntax function asr_bv "(bvashr %1 %2)"
(* remove prop asr_bv_is_asr *)
syntax function lsl_bv "(bvshl %1 %2)"
(* remove prop lsl_bv_is_lsl *)
remove prop to_uint_lsl
remove prop Extensionality
(** rotations *)
(* remove prop rotate_left_bv_is_rotate_left *)
(* remove prop rotate_right_bv_is_rotate_right *)
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
(** nth_bv *)
(* remove prop nth_bv_def *)
(* remove prop Nth_bv_is_nth *)
(* remove prop Nth_bv_is_nth2 *)
remove prop Extensionality
end
theory bv.BV64
......@@ -88,6 +125,8 @@ theory bv.BV64
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function size_bv "(_ bv64 64)"
syntax predicate is_signed_positive "(bvsge %1 (_ bv0 64))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
end
......@@ -103,6 +142,8 @@ theory bv.BV32
syntax function ones "#xFFFFFFFF"
syntax function size_bv "(_ bv32 32)"
syntax predicate is_signed_positive "(bvsge %1 (_ bv0 32))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
end
......@@ -118,6 +159,8 @@ theory bv.BV16
syntax function ones "#xFFFF"
syntax function size_bv "(_ bv16 16)"
syntax predicate is_signed_positive "(bvsge %1 (_ bv0 16))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
end
......@@ -133,6 +176,8 @@ theory bv.BV8
syntax function ones "#xFF"
syntax function size_bv "(_ bv8 8)"
syntax predicate is_signed_positive "(bvsge %1 (_ bv0 8))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
end
......
(**********************************************************************
*** gnat2why theories ***
**********************************************************************)
theory _gnatprove_standard_th.Floating_Func
syntax predicate neq "(not (fp.eq %1 %2))"
syntax function bool_lt "(fp.lt %1 %2)"
syntax function bool_le "(fp.leq %1 %2)"
syntax function bool_gt "(fp.gt %1 %2)"
syntax function bool_ge "(fp.geq %1 %2)"
syntax function bool_eq "(fp.eq %1 %2)"
syntax function bool_neq "(not (fp.eq %1 %2))"
remove allprops
end
(*************************************************************************)
theory "_gnatprove_standard".Floating
syntax function rem "(fp.rem %1 %2)"
syntax function div_rne "(fp.div RNE %1 %2)"
remove allprops
end
theory "_gnatprove_standard".Float32_next_prev
syntax function max_value "(fp #b0 #b11111110 #b11111111111111111111111)"
end
theory "_gnatprove_standard".Float64_next_prev
syntax function max_value "(fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111)"
end
theory "_gnatprove_standard".Float32
syntax function one "(fb #b0 #b01111111 #b00000000000000000000000)"
remove allprops
end
theory "_gnatprove_standard".Float64
syntax function one "(fb #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)"
remove allprops
end
(*************************************************************************)
theory ada__model.Floating_Point_Base
syntax function bool_eq "(fp.eq %1 %2)"
remove allprops
end
(*************************************************************************)
theory ieee_float.Float64
(* function to_int *)
end
theory ieee_float.Float32
(* function to_int *)
end
theory real.Square
remove allprops
end
......@@ -5,6 +5,8 @@ theory ieee_float.RoundingMode
syntax function RTP "RTP"
syntax function RTN "RTN"
syntax function RTZ "RTZ"
syntax predicate to_nearest "(or (= %1 RNE) (= %1 RNA))"
end
theory ieee_float.GenericFloat
......@@ -41,7 +43,12 @@ theory ieee_float.GenericFloat
syntax predicate is_positive "(fp.isPositive %1)"
syntax predicate is_negative "(fp.isNegative %1)"
syntax predicate is_finite "(not (or (fp.isInfinite %1) (fp.isNaN %1)))"
(* We could do this here, but we get slightly slimmer VCs and avoid
issues with Z3 if we do specialised versions of this for Float32 and
Float64 *)
(* The proposed fp.isFinite would fix all this. *)
(* syntax predicate is_finite "(not (or (fp.isInfinite %1) (fp.isNaN %1)))" *)
syntax predicate is_not_nan "(not (fp.isNaN %1))"
syntax function to_real "(fp.to_real %1)"
......@@ -62,6 +69,10 @@ theory ieee_float.Float32
syntax function zeroF "((_ to_fp 8 24) #x00000000)"
prelude "(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))"
syntax predicate t'isFinite "(fp.isFinite32 %1)"
remove allprops
end
......@@ -73,6 +84,10 @@ theory ieee_float.Float64
syntax function zeroF "((_ to_fp 11 53) #x0000000000000000)"
prelude "(define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))"
syntax predicate t'isFinite "(fp.isFinite64 %1)"
remove allprops
end
......
(**********************************************************************
*** gnat2why theories ***
**********************************************************************)
theory _gnatprove_standard_th.Integer
syntax function bool_eq "(= %1 %2)"
syntax function bool_ne "(not (= %1 %2))"
syntax function bool_lt "(< %1 %2)"
syntax function bool_le "(<= %1 %2)"
syntax function bool_gt "(> %1 %2)"
syntax function bool_ge "(>= %1 %2)"
remove allprops
end
theory _gnatprove_standard_th.Boolean_Func
syntax function bool_eq "(= %1 %2)"
remove allprops
end
(*************************************************************************)
theory _gnatprove_standard.BVAda
syntax function bool_eq "(= %1 %2)"
syntax function bool_ne "(not (= %1 %2))"
syntax function bool_lt "(bvult %1 %2)"
syntax function bool_le "(bvule %1 %2)"
syntax function bool_gt "(bvugt %1 %2)"
syntax function bool_ge "(bvuge %1 %2)"
remove allprops
end
(*************************************************************************)
theory ada__model.Discrete_Base
syntax function bool_eq "(= %1 %2)"
remove allprops
end
(*************************************************************************)
theory ada__model_th.Discrete_Base_Theory
syntax function bool_eq "(= %1 %2)"
remove allprops
end
......@@ -9,6 +9,7 @@ model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "z3_bv.gen"
import "smt-libv2-floats.gen"
import "discrimination.gen"
......@@ -77,41 +78,6 @@ theory real.Trigonometry
end
*)
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory ieee_float.Float64
(* check the sign bit; if pos |%1| else |%1| - 2^1025 *)
syntax function to_int
......
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV_Gen
syntax function to_uint "(bv2int %1)"
end
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
......@@ -2,30 +2,36 @@
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require bool.Bool.
Require int.Int.
Require map.Map.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype .
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype.
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value .
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value.
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator