Read Allan Blanchard's Frama-C tutorial at least up to section 4.4.1.
Strive to get Frama-C installed —
opam install alt-ergo altgr-ergo why3 frama-c on a Linux machine
should work (after you installed opam).
Documentation is under “Support”;
start familiarising yourself with the
ACSL Reference Manual — current Frama-C support version.
For your own examples, the following C module organisation is strongly recommended:
.h interface files.
A “library implementation” in a .c file imports the
corresponding .h file.
Library functions that perform I/O should be kept in separate modules.
main.c driver typically includes stdio.h and performs some I/O
(typically at least sone printf() calls),
and contains as little non-I/O material as possible.Please log your (possibly incomplete!) experiments in a LaTeX document; please document your problems, and if applicable, alternatives you explored. For pretty-printing of ACSL and ACSL-annotated C-code, use listingsACSL.sty (improvements welcome!) in the following way:
\usepackage{listings}
\usepackage{listingsACSL}
...
\lstset{language=[ACSL]C,...}
Continue the quest started in the lecture: Declare, specify, implement, annotate, and verify a C function +binsearch= for binary search using ACSL.
Program “the four plausible versions of fib” as
C functions calculating the Fibonacci numbers.
Add ACSL specifications and annotations to verify them.
(You will need a logic function Fib that maps each natural number
n to the nth Fibonacci number.
In the Jan. 30 lecture, the How to Verify IoT Software with Frama-C slides (see also the corresponding brief paper) were presented up to slide 64 presenting contracts; work through the following slides 65–67 and include your answers to the questions posed there in your document. Continue to work also through the loop annotation section (slides 69–80), and strive to solve Examples 7--9 yourself before you proceed to look at the solutions.
Continuing in the
How to Verify IoT Software with Frama-C
slides,
strive to make sense of the memb_alloc example (slides 81–85) —
try to formalise the specification of memb-alloc starting from
the informal description at the bottom of slide 84,
and to complete the annotation following the hints on slide 85.
Read also the following “My proof fails... What to do?” section.