Open source case studies for Frama-C
====================================
This repository is a collection of open source C codes to be used with
[Frama-C](http://frama-c.com), 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.7.
# 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
(in `frama-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. Running `fcmake` will run Frama-C related targets;
running `make` will run the case study's original Makefile (if it exists).
- `cd` to the subdirectory of one of the case studies;
We recommend `2048` for a short and fast analysis, or `debie1` 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 subdirectories
`t.parse` for parsing and `t.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-run `fcmake`.
# Notes
A summary of the case studies, with a brief description, URL, number of Eva
targets, etc, is available at [summary.md](summary.md).
## 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 a `GNUmakefile` 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.
- Some Makefiles were renamed `Makefile.original`, and a simplified
OSCS-related `Makefile` has been added. This enables compiling some targets
in a way that is useful for certain build tools.
In case studies related to benchmarking, examples or test suites, we often
apply modifications more liberally.
## Rationale
The main objectives of these files are:
1. Non-regression tests;
2. Benchmarking;
3. 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`: see `LICENSE`
- `bench-moerman2018`: MIT
- `c-testsuite`: see `LICENSE` and `LICENSE-tests`
- `c-utils` : MIT
- `cerberus`: see `LICENSE`
- `chrony`: GPL
- `debie1`: distribution and use authorized by Patria Aviation Oy,
Space Systems Finland Ltd. and Tidorum Ltd, see `README.txt`
and `terms_of_use-2014-05.pdf`
- `genann`: Zlib, see `LICENSE`
- `gnugo`: GPL
- `gzip124`: GPL
- `hiredis`: Redis license (BSD-style), see `COPYING`
- `icpc`: Unlicense
- `ioccc`: Creative Commons Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0),
see `COPYING`
- `itc-benchmarks`: BSD 2-clause, see `COPYING`
- `jsmn`: MIT
- `kgflags`: MIT, see `LICENSE`
- `khash`: MIT
- `kilo`: BSD 2-clause "Simplified", see `LICENSE`
- `libmodbus`: LGPL
- `libspng`: BSD 2-clause, see `LICENSE`
- `libyaml`: MIT, see `License`
- `line-following-robot`: MIT + modified BSD (for included `avr-libc`),
see `LICENSE` and `avr-libc/include/LICENSE`
- `mibench`: several, see `LICENSE` file inside each subdirectory
- `mini-gmp`: LGPL or GPL
- `miniz`: MIT
- `microstrain`: GPL and others, see `LICENSE`
- `monocypher`: see `README`
- `papabench`: GPL
- `polarssl`: GPL
- `powerwindow`: GPL
- `qlz`: GPL
- `safestringlib`: MIT
- `semver`: MIT
- `solitaire`: public domain, see `solitaire.c`
- `stmr`: MIT
- `tsvc`: MIT, see `license.txt`
- `tweetnacl-usable`: public domain, see `LICENSE.txt`
- `verisec`: several, according to each app
- `x509-parser` : GPLv2 / BSD, see `LICENSE`
# Troubleshooting / Debugging
(This section is mainly for Frama-C/plug-in developers who want to test OSCS
with specific versions of Frama-C)
OSCS can work in different modes:
1. With a local Frama-C, installed via the Git submodule 'frama-c'
(after running `make framac`);
2. With another, locally-installed Frama-C;
3. With Frama-C installed in the PATH.
This behavior is defined in `path.mk`. This file is included (as a symbolic
link) in the `.frama-c` directory for each case study. Changing this file will
change the behavior of all case studies.
- Mode 1 (by default) is enabled as soon as `make framac` is executed.
- To enable mode 2, modify the `FRAMAC_DIR=` line in `path.mk` to point to the
`bin` directory of your locally installed Frama-C.
- To enable mode 3, simply comment the `FRAMAC_DIR=` line.
If the value of `FRAMAC_DIR` is invalid (does not point to an existing
directory), an error will be raised.
If you need help debugging, consider adding messages such as
`$(info FRAMAC_DIR is: $(FRAMAC_DIR))` to `path.mk`.
When running one of the `make` targets, these messages might help understand
if the path has been properly set.