Open source case studies for Frama-C
This repository is a collection of open source C codes to be used with Frama-C, in particular with the Eva (Evolved Value Analysis) plug-in.
Most directories contain open-source code that constitutes a "case study". A few contain sets of tests, benchmarks or tutorials.
Requirements
- GNU Make >= 4.0;
- (optional, for some scripts) Python >= 3.6.
Basic usage
-
(required once)
make submodules
: initializes the local Frama-C submodule; -
(required once)
make framac
: prepares a git submodule with a clone of the public git of Frama-C, compiles it and installs it locally (inframa-c/build/bin
); -
(required once) add the following alias to your shell:
alias fcmake='make -C .frama-c'
Each "case study" contains a
.frama-c
subdirectory with the Frama-C Makefile. Runningfcmake
will run Frama-C related targets; runningmake
will run the case study's original Makefile (if it exists). -
cd
to the subdirectory of one of the case studies; We recommend2048
for a short and fast analysis, ordebie1
for a finalized analysis. -
Run
fcmake
to parse and run Eva on the predefined targets.
Makefile targets
The scripts provided with Frama-C create several Makefile targets, according to the intended usage. The main ones are:
-
display-targets
: lists the base targets - For each base target
t
, the following targets are generated:-
t.parse
: parse the sources; -
t.eva
: run Eva; -
t.eva.gui
: open the GUI.
-
Each target depends on the previous one: running t.eva.gui
will
automatically run t.eva
if required; the same for t.parse
.
Other generated targets:
-
t.parse.gui
: open the GUI with the result of the parsing, without running Eva. Mostly useful in conjunction with other plug-ins. -
t.stats
: print time/memory usage.
Remarks
- The output of
t.eva
is verbose, but you can ignore it; the important information (warnings and alarms) can be inspected via the GUI. - The result of the analysis is stored inside
.frama-c
, in subdirectoriest.parse
for parsing andt.eva
for the Eva analysis. Each subdirectory contains a few log files. - To try other parametrizations, simply edit variables
CPPFLAGS/FCFLAGS/EVAFLAGS
in.frama-c/GNUmakefile
and re-runfcmake
.
Notes
Source code modifications
We attempt to minimize changes to each case study, to keep the code close to the original. Here are the most common kinds of changes:
- A
.frama-c
directory is added, with aGNUmakefile
which defines the Frama-C targets and parameters; - Some stubs file (e.g.
stubs.c
) are added to the.frama-c
directory, either to emulate an initial state with command-line arguments, or to provide code/specifications for library functions, missing code, non-portable features, etc. - When code modifications are needed (and cannot be moved to the stubs file,
e.g. when adding a specification to a
static
functions), we often protect them by#ifdef __FRAMAC__
guards, to ensure the code compiles as before when not using Frama-C. Note that this is not always the case. - Some unnecessary files for the analysis (e.g. documentation, project setups for IDEs, non-code resources) are removed.
In case studies related to benchmarking, examples or test suites, we often apply modifications more liberally.
Rationale
The main objectives of these files are:
- Non-regression tests;
- Benchmarking;
- Practical examples.
Therefore, some of the code bases are voluntarily parametrized with suboptimal parameters, for non-regression testing. Some code bases undergo partial, progressive improvements. Only a few constitute "finalized" case studies.
Contributions
If you know of other open source code bases where Frama-C/Eva produces
interesting results, please contribute with pull requests including the
case study sources and your .frama-c/GNUmakefile
.
On the other hand, if you have some interesting open-source C software (ideally, C99-compatible) that you are unable to parse and/or run with Frama-C/Eva, consider creating an issue in this repository¹ with the description of the problem you are facing (e.g. missing/incompatible declarations in the Frama-C libc, problems when preprocessing/parsing the code, constructs unsupported by Eva, etc). Ideally, create a (WIP) pull request with the sources in a new directory, ready to be prepared for the case study.
¹ Note: direct account creation is disabled in Frama-C's Gitlab; linking a Github account is always possible.
License
License files are kept in each directory where they were originally found, when available. We also summarize the license of each directory below.
-
2048
: MIT -
basic-cwe-examples
: seeLICENSE
-
bench-moerman2018
: MIT -
c-testsuite
: seeLICENSE
andLICENSE-tests
-
cerberus
: seeLICENSE
-
chrony
: GPL -
debie1
: distribution and use authorized by Patria Aviation Oy, Space Systems Finland Ltd. and Tidorum Ltd, seeREADME.txt
andterms_of_use-2014-05.pdf
-
genann
: Zlib, seeLICENSE
-
gzip124
: GPL -
hiredis
: Redis license (BSD-style), seeCOPYING
-
icpc
: Unlicense -
ioccc
: Creative Commons Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0), seeCOPYING
-
itc-benchmarks
: BSD 2-clause, seeCOPYING
-
jsmn
: MIT -
kgflags
: MIT, seeLICENSE
-
khash
: MIT -
kilo
: BSD 2-clause "Simplified", seeLICENSE
-
libmodbus
: LGPL -
libspng
: BSD 2-clause, seeLICENSE
-
libyaml
: MIT, seeLicense
-
mibench
: several, seeLICENSE
file inside each subdirectory -
mini-gmp
: LGPL or GPL -
miniz
: MIT -
microstrain
: GPL and others, seeLICENSE
-
monocypher
: seeREADME
-
papabench
: GPL -
polarssl
: GPL -
qlz
: GPL -
safestringlib
: MIT -
semver
: MIT -
solitaire
: public domain, seesolitaire.c
-
tsvc
: MIT, seelicense.txt
-
tweetnacl-usable
: public domain, seeLICENSE.txt
-
x509-parser
: GPLv2 / BSD, seeLICENSE