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] Jessie: Local variables leading to

On 10/17/10, Norbert M?ller <mueller at uni-trier.de> wrote:

> I try to verify a C program with local variables that are passed
> to
> subroutines using the address operator.

Another way to nudge the Why file generation into working is
apparently to use the following line at the top of your file:

#pragma SeparationPolicy(none)

This has the same effect as the previous, now obsolete option
-jessie-no-regions documented in the online manual, chapter 5:
http://frama-c.com/jessie/jessie-tutorial.pdf

(by the way there is an updated version of this manual, we just have
to think to upload it someday)

Like removing the assigns clauses, this changes the assumptions made
by Jessie, and may make your reduced example, or indeed your real
target program, unprovable. I am not quite competent enough to tell if
this is the case on the reduced example.

I do recommend that you upgrade to Why 2.27; there were a number of
bugfixes and improvements since Why 2.24.

Best regards,

Pascal