--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on May 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New user questions



Hello,

  My name is Mike Whalen and I work at Amazon.  I am looking at potentially using Frama-C for verification of some of the C code that we use.  I am working my way through the Frama-C WP tutorial for version 20.0 (the March 30, 2020 edition).  I have a few questions related to installation, different solvers, and debugging.  I am running on Mac OS X 10.14.6.

For installation, I can run the frama-c command line tool and the frama-c-gui, but I can’t invoke WP from within the GUI.  I can run WP from the command line and the proof goals are annotated properly, but the WP panel on the left side of the GUI does not provide a button to ‘prove’ as it does in the tutorial, as shown in the attached screen shot.  For the moment, I am making do with the command line tool.

For different solvers, I get different answers from alt-ergo and z3 for the same properties, with z3 timing out or failing on a handful of goals that alt-ergo succeeds on.  I would expect differences in timeouts between solvers (e.g., one times out but not the other), but not discrepancies as to whether obligations are true or false.  Perhaps ‘failure’ in this case simply means ‘failure to prove’.  I am running z3 4.8.4 and alt-ergo 2.3.2.  I am attaching the .c and .h files.  The command lines are:

frama-c -rte -wp -wp-prover z3 skip.c

frama-c -rte -wp -wp-prover alt-ergo skip.c

Finally, for debugging is there any kind of symbolic debugger or way to get counterexample information?  The VeriFast tool has a nice IDE where you can forward/back-step through a program with a symbolic heap.  At the moment, when a proof fails, I just stare hard at it and try to figure out how to fix it, but I would expect power-users have a few more things in their bag of tricks.  The WP tutorial did not have a lot of information on this aspect.

Thank you very much for any help!  I am having fun with frama-c and look forward to learning how to use it effectively.

Best regards,

Mike
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200501/4ba81603/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2020-05-01 at 1.08.19 PM.png
Type: image/png
Size: 311731 bytes
Desc: Screen Shot 2020-05-01 at 1.08.19 PM.png
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200501/4ba81603/attachment-0001.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: jsonparser.h
Type: application/octet-stream
Size: 6643 bytes
Desc: jsonparser.h
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200501/4ba81603/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: skip.c
Type: application/octet-stream
Size: 4334 bytes
Desc: skip.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200501/4ba81603/attachment-0003.obj>