Dear Jean-Jacques,
> not sure I got the semantics of ‘ghost expr’. Is it described in
> manual 0.82 ?
We forgot to mention the existence of a recent paper of ours describing
the notion of ghost code currently implemented in Why3:
http://hal.inria.fr/hal-00873187
Though it mostly describes the
Hello!
I am trying to use some why3 functionalities into a frama-c plugin
that I developed.
Is there any way to create why3 sessions using the command line?
The idea is that I have a list of .c files and I want to call jessie
for all of these files and then generate a report for each one of
the
On Thu, 13 Feb 2014 14:50:32 +0100, Andrei Paskevich wrote:
In this case, I don't think I agree with you. The variable tmp
*occurs* in the expression but is not really *used*, and it's exactly
a kind of possible non-evident mistake you want to be warned of.
I agree that there should be a warni
On 13 February 2014 11:53, Johannes Kanig wrote:
> On Wed, 12 Feb 2014 11:28:50 +0100, Andrei Paskevich wrote:
>>
>> Fixed in git, thanks for the report.
>
> Thanks again, however I still have a slight variant of this warning:
>
>
> module M
> use import "int".Int
> use import "ref".Ref
>
> ty
On Wed, 12 Feb 2014 11:28:50 +0100, Andrei Paskevich wrote:
Fixed in git, thanks for the report.
Thanks again, however I still have a slight variant of this warning:
module M
use import "int".Int
use import "ref".Ref
type rec1t = { rec__f1 : int; rec__g1 : int }
val r : ref rec1t
le
Dear Why3 Friends,
recently ‘why3ide’ got new behavior on my Macbook Air. Fonts to the left get
very large. And I cannot find way to reduce their size. Maybe it’s X-server
which changed. Don’t know that happened. Anyone with same problem ?
Furthermore, I cannot remember way to set preferences f
