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] A toy electronic voting software checked with Frama-C
- Subject: [Frama-c-discuss] A toy electronic voting software checked with Frama-C
- From: dmentre at linux-france.org (David MENTRE)
- Date: Fri, 27 Mar 2009 10:30:15 +0100
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 : ). 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 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  http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000465.html  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
- Prev by Date: [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparisonexample
- Next by Date: [Frama-c-discuss] Semantics of Jessie icons?
- Previous by thread: [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparisonexample
- Next by thread: [Frama-c-discuss] HELP FRAMA-C