--- layout: fc_discuss_archives title: Message 75 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



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