--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on November 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] (no subject)




On 11/01/2014 07:10 PM, gavran at mpi-sws.org wrote:
> Thank you for the answer, Clauude. Yes, "new_value" is my attempt to mimic
> malloc (I abstracted the details out). Reason why I started doing it in
> the first place was that WP displayed the warning: "warning: Allocable,
> Freeable, Valid_read, Fresh and Initialized not yet implemented".
> As it is under "experimental" section in ACSL documentation, I concluded
> it is just not yet implemented.

More precisely: these "experimental" ACSL clauses *are implemented in 
Frama-C kernel*. But they may not be supported by plug-ins. If the 
warning above is issued with the last version of WP, then yes it means 
these are not supported by WP.

> (I have problems with Jessie, it crashes and I still don't get why, so I
> couldn't try with it.).

We can't help if you do not provide more details...

> Which prover do you use? (that supports those "experimental" features)

This support is not dependent on which prover you use. This is supported 
by Jessie "experimentally", meaning that problems may show up, such as 
when you do not provide the pragma SeparationPolicy(none)

With this pragma, the file as I gave it in my previous mail is fully 
proved by Frama-C/Jessie/Why3 + any prover like Alt-Ergo, CVC4, Z3.

- Claude