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

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