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 : [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