Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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