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