 18 Apr, 2015 4 commits


MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

 17 Apr, 2015 14 commits



Mário Pereira authored

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

git+ssh://scm.gforge.inria.fr//gitroot/why3/why3Martin Clochard authored
Conflicts: examples/verifythis_2015_relaxed_prefix/why3session.xml examples/verifythis_2015_relaxed_prefix/why3shapes.gz

Martin Clochard authored

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored


Martin Clochard authored

MARCHE Claude authored

JeanChristophe Filliâtre authored
in comments for the moment, until I find time to prove it

MARCHE Claude authored

MARCHE Claude authored

 16 Apr, 2015 2 commits


JeanChristophe Filliâtre 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 8 commits


David Hauzar authored

David Hauzar authored

David Hauzar authored
Conflicts: src/ide/gmain.ml

David Hauzar authored

Martin Clochard authored

David Hauzar authored
Conflicts: drivers/cvc4_bare.drv share/proversdetectiondata.conf src/driver/driver_parser.mly src/printer/smtv2.ml

MARCHE Claude authored

Mário José Parreira Pereira authored

 14 Apr, 2015 1 commit


David Hauzar authored

 13 Apr, 2015 6 commits


David Hauzar authored

David Hauzar authored
p labeled with label "model_projected" for that it exists a projection function f creates declaration of new constant c and axiom stating that c = f p Projection functions are functions tagged with meta "model_projection". Function f is projection function for abstract function and predicate p if f is tagged with meta "model_projection" and has a single argument of the same type as is the type of p. This transformation is needed in situations when we want to display not value of a variable, but value of a projection function applied to a variable. Note that since Why3 supports namespaces (different projection functions can have the same name) and input languages of solvers typically not, Why3 renames projection functions to avoid name clashes. This is why it is not possible to just store the name of the projection function in a label and than query the solver directly for the value of the projection. Also, it means that this transformation should thus be executed before this renaming.

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

 12 Apr, 2015 2 commits


JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

 11 Apr, 2015 2 commits


Andrei Paskevich authored
1. Strong region updates can only work with direct assignments, e.g. r.contents < something_completely_different but not with functions such as (:=) : ref 'a > 'a > unit Why3 requires 'a to be instantiated with one concrete type, not with a bunch of types that differ in their regions. 2. Strong region updates will restrict the updated regions to their covers. However, in the current implementation, Why3 does not know if the region corresponding to the field "contents" is the only cover for 'a in the type [ref 'a] or if there is a way to retrieve 'a from [ref 'a] without going through "contents". Therefore, to ensure soundness, a strong update of r.contents will forbid to use r itself. A solution consists in writing an adhoc "reference" type, where the mutable contents (O.t in this case) is explicitly given in the type definition. Then the strong update of the field containing O.t will preserve the covering "reference". This problem is fixed in the "new system", where mutable types carry information about the access paths of the type variables. There, "r.contents < something_different" preserves r.

JeanChristophe Filliâtre authored

 10 Apr, 2015 1 commit


MARCHE Claude authored
