--- layout: fc_discuss_archives title: Message 75 from Frama-C-discuss on November 2009 ---
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", line 735, characters 1-1: Uncaught exception: File "jc/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": -------------------------------- 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", line 1824, characters 19-19: Uncaught exception: File "jc/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> > > 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 > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091123/17f6fcc8/attachment.htm