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] New user questions

  • Subject: [Frama-c-discuss] New user questions
  • From: mww at amazon.com (Whalen, Mike)
  • Date: Fri, 1 May 2020 18:29:28 +0000
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>