Commit 587c4b4d authored by Thibault Martin's avatar Thibault Martin
Browse files

Merge branch 'master' into ltest-experimental

parents b2d3f506 6d12e258
Pipeline #36749 failed with stage
in 31 seconds
......@@ -30,6 +30,6 @@ bench_clone
*_labels.c
*_NA
*_Eq
*_VA
*_WP
*_VA*
*_WP*
*_Candidate
default:
image: framac/frama-c:dev
image: framac/frama-c:dev-stripped
build:
tags:
......
......@@ -22,17 +22,24 @@ A few contain sets of tests, benchmarks or tutorials.
- (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`);
- `cd` to one of the case studies;
- (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 `make` to parse and run Eva on the predefined targets.
- 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:
- `help`: lists the base targets
- `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;
......@@ -51,37 +58,34 @@ Other generated targets:
- 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 each analysis is stored in a directory containing the full logs
and Frama-C save files; successive runs are copied into timestamped
directories, to allow comparing them (e.g. via `meld`);
- 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 `GNUmakefile` and re-run `make`.
- Technical remark: the default file used by GNU Make is `GNUmakefile`,
if it exists.
We use this to avoid renaming the original Makefile, if any. It also means
that, if you want to *compile* the code using its Makefile, you have to
explicitly name it (e.g. `make -f Makefile`).
`CPPFLAGS/FCFLAGS/EVAFLAGS` in `.frama-c/GNUmakefile` and re-run `fcmake`.
# Notes
## Source code modifications
Only minor modifications were performed on each of these case studies:
- File `GNUmakefile` is added to each case study, with Frama-C/Eva-specific
rules for parsing and running the analysis;
- When necessary, syntactic modifications were performed to ensure better
C99-compliance and/or the inclusion of stubs to allow Frama-C to parse the
files;
- In some cases, an `eva_main` function was added to provide a better initial
context for the analysis;
- When recursive calls are present, the functions containing them need to be
replaced with specifications;
- Some ACSL annotations were added to the sources
(to illustrate their usage, or to improve the analysis);
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) were removed.
for IDEs, non-code resources) are removed.
In case studies related to benchmarking, examples or test suites, we often
apply modifications more liberally.
## Rationale
......@@ -100,7 +104,7 @@ Only a few constitute "finalized" case studies.
If you know of other open source code bases where Frama-C/Eva produces
interesting results, please contribute with pull requests including the
sources and the `GNUmakefile` that you have devised to run Frama-C.
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
......@@ -123,6 +127,8 @@ 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`
- `cerberus`: see `LICENSE`
- `chrony`: GPL
- `debie1`: distribution and use authorized by Patria Aviation Oy,
Space Systems Finland Ltd. and Tidorum Ltd, see `README.txt`
......@@ -137,12 +143,11 @@ when available. We also summarize the license of each directory below.
- `jsmn`: MIT
- `kgflags`: MIT, see `LICENSE`
- `khash`: MIT
- `kilo`: BSD 2-clause "Simplified"
(see https://github.com/antirez/kilo/blob/master/LICENSE)
- `kilo`: BSD 2-clause "Simplified", see `LICENSE`
- `libmodbus`: LGPL
- `libspng`: BSD 2-clause, see `LICENSE`
- `libyaml`: MIT, see `License`
- `mibench`: several (see `LICENSE` file inside each subdirectory)
- `mibench`: several, see `LICENSE` file inside each subdirectory
- `mini-gmp`: LGPL or GPL
- `miniz`: MIT
- `microstrain`: GPL and others, see `LICENSE`
......@@ -152,6 +157,7 @@ when available. We also summarize the license of each directory below.
- `qlz`: GPL
- `safestringlib`: MIT
- `semver`: MIT
- `solitaire`: public domain (see `solitaire.c`)
- `tweetnacl-usable`: public domain (see `LICENSE.txt`)
- `x509-parser` : GPLv2 / BSD (see `LICENSE`)
- `solitaire`: public domain, see `solitaire.c`
- `tsvc`: MIT, see `license.txt`
- `tweetnacl-usable`: public domain, see `LICENSE.txt`
- `x509-parser` : GPLv2 / BSD, see `LICENSE`
......@@ -43,7 +43,7 @@ include ../../Makefile.ltest
$(eval $(call generate-rules,cwe787,../cwe787.c))
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
include $(FRAMAC_SHARE)/analysis-scripts/epilogue.mk
###############################################################################
# optional, for OSCS
......
directory file line function property kind status property
. cwe588.c 10 main mem_access Invalid or unreachable \valid(&foo->i)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 1)
Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
4 stmts in analyzed functions, 2 stmts analyzed (50.0%)
main: 2 stmts out of 4 (50.0%)
cwe588.c:10:[nonterm:stmt] warning: non-terminating statement
stack: main
cwe588.c:10:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
/* Generated by Frama-C */
struct foo {
int i ;
};
int main(void)
{
int __retres;
struct foo *foo = (struct foo *)(& main);
foo->i = 2;
__retres = foo->i;
return __retres;
}
[metrics] Defined functions (1)
=====================
main (address taken) (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (0)
==========================
Global metrics
==============
Sloc = 4
Decision point = 0
Global variables = 0
If = 0
Loop = 0
Goto = 0
Assignment = 3
Exit point = 1
Function = 1
Function call = 0
Pointer dereferencing = 2
Cyclomatic complexity = 1
cwe588.c:9:[kernel:typing:incompatible-pointer-types] warning: casting function to struct foo *
directory file line function property kind status property
. cwe588.c 10 main mem_access Invalid or unreachable \valid(&foo->i)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 1)
Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
4 stmts in analyzed functions, 2 stmts analyzed (50.0%)
main: 2 stmts out of 4 (50.0%)
cwe588.c:10:[nonterm:stmt] warning: non-terminating statement
stack: main
cwe588.c:10:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
/* Generated by Frama-C */
struct foo {
int i ;
};
int main(void)
{
int __retres;
struct foo *foo = (struct foo *)(& main);
foo->i = 2;
__retres = foo->i;
return __retres;
}
[metrics] Defined functions (1)
=====================
main (address taken) (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (0)
==========================
Global metrics
==============
Sloc = 4
Decision point = 0
Global variables = 0
If = 0
Loop = 0
Goto = 0
Assignment = 3
Exit point = 1
Function = 1
Function call = 0
Pointer dereferencing = 2
Cyclomatic complexity = 1
cwe588.c:9:[kernel:typing:incompatible-pointer-types] warning: casting function to struct foo *
directory file line function property kind status property
. cwe761.c 24 contains_char precondition of free Invalid or unreachable freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Invalid or unreachable freeable: p ≡ \null ∨ \freeable(p)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 2 (out of 2)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
21 stmts in analyzed functions, 15 stmts analyzed (71.4%)
main: 2 stmts out of 2 (100.0%)
contains_char: 13 stmts out of 19 (68.4%)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment