 20 Aug, 2015 40 commits


Andrei Paskevich authored
except for modules/impset.mlw (because of Fset) and modules/mach/* (because of program cloning), the standard library now typechecks. This is still very much the work in progress. Many functions and predicates have still to be converted to "let function" and "let predicate". Here are some TODOs:  do not require the return type for "val predicate", "val lemma", etc.  do not require explicit variant for "let rec" if the code passes the termination check in Decl (see list.why)  what should become "val ghost function" and what should stay just "function" (see array.mlw, matrix.mlw, string.mlw, etc)?  some defined functions in algebra.why and relations.why had to be removed, so that they can be implemented with "let function" in int.mlw (since they are defined, they cannot be instantiated with letfunctions). This seems too restrictive. One way out would be to authorise instantiation of defined functions (with a VC).  should we keep the keyword "model"? reuse of "abstract" in types breaks syntax coloring ("abstract" requires closing "end" in programs but not in types; maybe we can drop that "end" again?).

 29 May, 2015 40 commits


David Hauzar authored

MARCHE Claude authored
Signedoffby: Claude Marche <Claude.Marche@inria.fr>

David Hauzar authored
Move of the transformations introduce_premises and intro_projections_counterexmp to the end of the driver. Note that this requires putting meta "inline : no" for every projection function to the source file. Otherwise, declarations projection functions are removed and the transformation intro_projections_counterexmp fails.

 28 May, 2015 40 commits


Clément Fumex authored
 generation in the makefile  proofs done Remove complex axioms from Pow2int in bv.why. Add guards in rotates axioms in bv.why.

 26 May, 2015 40 commits


MARCHE Claude authored
This should restore the current failing replay of nightly bench

MARCHE Claude authored

David Hauzar authored
If these are set, the prover is asked for counterexample and if the counterexample is got, it is displayed.

 23 May, 2015 40 commits


Andrei Paskevich authored

 21 May, 2015 40 commits


MARCHE Claude authored
since results are better with the Why3 axiomatic version

 19 May, 2015 40 commits


MARCHE Claude authored

MARCHE Claude authored

 18 May, 2015 40 commits


MARCHE Claude authored

MARCHE Claude authored

David Hauzar authored

 06 May, 2015 40 commits


Clément Fumex authored

 23 Apr, 2015 40 commits


Stefan Berghofer authored

 22 Apr, 2015 40 commits


David Hauzar authored

 18 Apr, 2015 40 commits


MARCHE Claude authored

MARCHE Claude authored

 17 Apr, 2015 40 commits


MARCHE Claude authored

MARCHE Claude authored

 16 Apr, 2015 40 commits


JeanChristophe Filliatre authored
this is of course unsafe, yet useful if you have proved absence of overflows independently or if you are happy with a partial correctness proof (that is, if there is no overflow then the postcondition holds) this is work in progress; nothing plugged in yet

Clément Fumex authored

 15 Apr, 2015 40 commits


David Hauzar authored

 08 Apr, 2015 40 commits


Stefan Berghofer authored

 07 Apr, 2015 40 commits


MARCHE Claude authored

 02 Apr, 2015 40 commits


MARCHE Claude authored

MARCHE Claude authored

 25 Mar, 2015 40 commits


MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

 23 Mar, 2015 40 commits


MARCHE Claude authored
+ fixed wrong step limit in one session

 22 Mar, 2015 40 commits


MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

 19 Mar, 2015 40 commits


MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored
