--- layout: fc_discuss_archives title: Message 96 from Frama-C-discuss on March 2009 ---
Hello, Please find attached the source code of a toy electronic voting software checked with Frama-C. All properties are proven with Alt-Ergo except a few ones related to assign clauses (for which I made a separated test case : [1]). Usage: make test # to test the software make check # Frama-C/Jessie in command line make gui # Frama-C/Jessie in GUI I would be very grateful if somebody could read my Frama-C annotations and tell me about errors, inaccuracies or bad style. This is after all my first Frama-C program. ;-) This software does not pretend to be of any use. Even regarding the functionnalities of the program, several things could be improved or refined. The current code has the advantage of conciseness (about 300 lines of code) while keeping core functionalities (I/O and computations). My overall comments regarding Frama-C: * I'm rather pleased with the software. The documentation is useful (good index for ACSL) even if not complete (Jessie), the software is working and I had only a few blocking bugs. Once you know a few idoms (loop invariants, non terminating functions, ...), it is rather easy for a basic engineer like me to express properties and check them; * Frama-C/Jessie helped me to find bugs in my original program, either benign ones (e.g. the potential overflow of counters) or more serious ones (e.g. program behaviour when reading too short candidate list). * A working subset of the Frama-C ecosystem is Free Software, making easier to use it in various settings. I hope the few remaning licensing issues[2] will be cleared out, allowing inclusion of Frama-C into various Linux distributions; * On my program, Jessie/Alt-Ergo GUI are becoming a bit slow, compared to toy example I have tested. It might come from my particular program, the way I have written or structured the code. I would be interested to hear of any way I could improve this; * I haven't dug yet into the development of plugins or into the Frama-C GUI (slicing, ...) so I won't comment on them, even if they seem quite interesting. Thank you for the work your are doing, Sincerely yours, david [1] http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000465.html [2] http://lists.debian.org/debian-ocaml-maint/2009/02/msg00218.html -------------- next part -------------- Condorcet Voltaire Diderot -------------- next part -------------- A non-text attachment was scrubbed... Name: evoting.c Type: application/octet-stream Size: 11014 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090327/203d04b5/attachment-0003.obj -------------- next part -------------- A non-text attachment was scrubbed... Name: check_specs.h Type: application/octet-stream Size: 590 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090327/203d04b5/attachment-0004.obj -------------- next part -------------- A non-text attachment was scrubbed... Name: Makefile Type: application/octet-stream Size: 431 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090327/203d04b5/attachment-0005.obj