--- layout: fc_discuss_archives title: Message 81 from Frama-C-discuss on November 2009 ---
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