--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on October 2010 ---
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