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] Using Frama-C as Caduceus

The reason is that swap is first interpreted as if a and b were in 
different block, whereas you call it on pointers to the same block.
A work around is to add a precondition that restrict a and b to be in 
the same block, and anyway you need something to specify that they do 
not overlap, e.g

requires (a==b) || (a + size <= b) || (b + size <= a);


- Claude

??????? ?????? wrote:
> Thank you very much, Claude!
> 
> Well, I'm happy with the structure of Frama-C/Jessie output, I was just 
> confused by the difference in output PVS lemmas and their quantites. I 
> feel ashame for having asked before having read. :( Yes, I've already 
> learned about memory safety and separations of memory regions and all 
> that things, so I got close enough to Caduceus results to feel satisfied.
> 
> But currently I'm stuck with another problem. I have this 
> code: http://pastebin.org/56389 When I run it through Jessie it crashes 
> with the following diagnostic:
> 
> --------------------------------
> tester at ubuntu-vs:~/practice/jessie_sort$ frama-c -jessie -jessie-atp 
> goals sort.c
> [kernel] preprocessing with "gcc -C -E -I.  -dD sort.c"
> [jessie] Starting Jessie translation
> [kernel] No code for function memcmp, default assigns generated
> [jessie] Producing Jessie files in subdir sort.jessie
> [jessie] File sort.jessie/sort.jc written.
> [jessie] File sort.jessie/sort.cloc written.
> [jessie] Calling Jessie tool in subdir sort.jessie
> Generating Why function swap
> Generating Why function sort
> ** Jc_interp_misc.transpose_location_list: TODO: parameters **
> memory (mem-field(int_M),a_3)
> in memory set (mem-field(int_M),a_3)
> File "jc/jc_interp_misc.ml <http://jc_interp_misc.ml>", line 735, 
> characters 1-1:
> Uncaught exception: File "jc/jc_interp_misc.ml 
> <http://jc_interp_misc.ml>", line 735, characters 1-7: Assertion failed
> [jessie] user error: Jessie subprocess failed:    jessie  -why-opt 
> -split-user-conj  -v       -locs sort.cloc sort.jc
> --------------------------------
> 
> 
> If I add SeparationPolicy pragma, I have similar assertion fail, but 
> already in "jc_interp.ml <http://jc_interp.ml>":
> 
> --------------------------------
> tester at ubuntu-vs:~/practice/jessie_sort$ frama-c -jessie -jessie-atp 
> goals sort.c
> [kernel] preprocessing with "gcc -C -E -I.  -dD sort.c"
> [jessie] Starting Jessie translation
> [kernel] No code for function memcmp, default assigns generated
> [jessie] Producing Jessie files in subdir sort.jessie
> [jessie] File sort.jessie/sort.jc written.
> [jessie] File sort.jessie/sort.cloc written.
> [jessie] Calling Jessie tool in subdir sort.jessie
> Generating Why function swap
> File "jc/jc_interp.ml <http://jc_interp.ml>", line 1824, characters 19-19:
> Uncaught exception: File "jc/jc_interp.ml <http://jc_interp.ml>", line 
> 1824, characters 19-25: Assertion failed
> [jessie] user error: Jessie subprocess failed:    jessie  -why-opt 
> -split-user-conj  -v       -locs sort.cloc sort.jc
> --------------------------------
> 
> If I comment "sort" function or calls of "swap" inside "sort", 
> everything's ok.
> Jessie also runs smooth if I leave everything "as is" but comment "*a = 
> *b" and "*b = t" lines in swap.
> 
> It seems that this bug is well known for a 
> while: http://bts.frama-c.com/view.php?id=80 , and I've read your 
> comment that the root of evil is conversion from int32 to int. 
> Unfortunately, I don't have enough skill to dig into the whole Frama-C 
> sources at once; is there any quick way for me as for "dumb end-user" 
> (smile) to overcome this problem? Maybe adding some explicit casts to 
> pointers, or changing their types, or some other code modifications may 
> help?
> 
> Regards,
> Dmitry
> 
> 
> 2009/11/23 Claude Marche <Claude.Marche at inria.fr 
> <mailto:Claude.Marche at inria.fr>>
> 
> 
>     As a first step, to recover a file closer to the Caduceus one, you
>     should
>     select the unbound model for integers, and disable separation analysis.
> 
>     #pragma JessieIntegerModel(exact)
>     #pragma SeparationPolicy(None)
> 
>     - Claude
> 
>     Claude Marche wrote:
>      > Hopefully, the jessie plugin of Frama-C provides some improvement
>     over
>      > Caduceus. Clearly, there is no chance that you get exactly the same
>      > PVS file.
>      >
>      > Now, I understand that you think the PVS file obtained via
>      > Frama-C/Jessie/Why is significantly more complex than the one you got
>      > from Caduceus/Why. Indeed, we are willing to improve Frama-C/Jessie
>      > output if you request for precise feature wishes.
>      >
>      > - Claude
>      >
>      >
>      >
>      >
> 
> 
>     --
>     Claude March?                          | tel: +33 1 72 92 59 69
>     INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
>     Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
>     4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
>     F-91893 <http://www.lri.fr/~marche/F-91893> ORSAY Cedex            
>            |
> 
> 
> 
> 
> 
> 
> 
> 
>     _______________________________________________
>     Frama-c-discuss mailing list
>     Frama-c-discuss at lists.gforge.inria.fr
>     <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>     http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss