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] Proving Memory Safety of String Algorithms without Providing Loop Invariants

  • Subject: [Frama-c-discuss] Proving Memory Safety of String Algorithms without Providing Loop Invariants
  • From: giesl at informatik.rwth-aachen.de (Juergen Giesl)
  • Date: Mon, 20 Jan 2014 16:10:37 +0100
Dear all,

we are currently writing a paper on termination analysis of C programs with
pointer arithmetic and (low-level) memory access. As a precondition to
termination, our approach also proves memory-safety of the program.
Therefore, we would like to compare our implementation (in the AProVE tool)
to Frama-C.

We installed the following programs:

- frama-c Fluorine-20130401
- Jessie 2.33
- Why 2.33
- Why3 0.82
- Z3 4.0.0 (4.3.2 is not supported and other versions of Z3 are not
available)
- Yices 1.0.16

This almost corresponds to the recommendations given on
http://krakatoa.lri.fr/, except that we use Why3 0.82 instead 0.81 (since
0.81 was no longer available).

We would like to let Frama-C generate loop invariants by itself. To this
end, we also installed apron 0.9.10. We tried to compile Why (including
Jessie) with the option --enable-apron which would in turn allow us to
start Jessie with the option -jessie-infer-annot. But unfortunately, we did
not manage to compile Why with this option. The output of the compiler is
attached in why.err. Indeed, Yannick Moy told us that the code for loop
invariant generation was most likely removed from Why2.

For example, we formulated a very easy algorithm which simply traverses an
array in the file easy.c. Here, Frama-C with the Jessie plug-in can only
prove memory safety if one provides the loop invariant as an annotation.
Similarly, in the examples in
http://www.fokus.fraunhofer.de/de/sqc/_download_sqc/ACSL-by-Example.pdf,
the loop invariant is also given by an annotation in the code. Is there a
way to make Frama-C infer such loop invariants automatically (probably by
using a different plug-in)?

Our approach can in particular prove termination and memory safety of
algorithms operating on strings. For that reason, we were particularly
interested in the way that Frama-C treats these algorithms. In the attached
file strcpy.c we took the full axiomatisation of strlen from Yannick Moy's
PhD thesis. But Frama-C didn't manage to prove its memory-safety. Did we do
something wrong here (i.e., is there another way to analyze string
algorithms with Frama-C)?

Finally, we also attached a user-defined algorithm for computing the length
of a string (in the file strlenNoLoopInvariant.c). Claude Marche showed us
how to annotate the program in such way that Frama-C can prove its memory
safety. But is there also some way to make Frama-C succeed on such proofs
without providing a suitable loop invariant?

It would be great if you could provide us some help here soon, since we
would like to include the experiments in our paper, which we intend to
submit to IJCAR this week.

Thanks a lot and best regards
Juergen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140120/76c3f94c/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: easy.c
Type: text/x-csrc
Size: 253 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140120/76c3f94c/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: strcpy.c
Type: text/x-csrc
Size: 2203 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140120/76c3f94c/attachment-0001.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: strlenNoLoopInvariant.c
Type: text/x-csrc
Size: 167 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140120/76c3f94c/attachment-0002.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: why.err
Type: application/octet-stream
Size: 738 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140120/76c3f94c/attachment.obj>