Commit 1b7def1f authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'blog-old-frama-c-docker' into 'master'

[blog] new post about old Frama-C Docker images

See merge request !131
parents 69b71e04 36d244ec
Pipeline #38935 passed with stage
in 1 minute and 49 seconds
---
layout: post
author: André Maroneze
date: 2021-10-15 17:00 +0100
categories: docker
title: "Running old Frama-C versions from Docker images"
---
There are several reasons one might want to run an old version of Frama-C:
- to test some outdated plugin which is only compatible with a previous version;
- to re-run analyses mentioned in an old tutorial or blog post;
- to compare results between Frama-C versions;
- for nostalgia's sake.
Whatever the reason, it can take a while to prepare an opam switch with an older
OCaml compiler; configure and install external dependencies; etc.
For this reason, we uploaded to
[Frama-C's Docker Hub](https://hub.docker.com/r/framac/frama-c/tags) a set of
images, going all way back to version 5 (Boron, from 2010). These are
tagged `framac/frama-c:X.Y-stripped`, and they have a working `frama-c` binary
(with lots of cruft removed to ensure a minimal image size) with the standard
open-source plug-ins distributed at the time.
Of course, most users will prefer running the latest Frama-C version, available
under several tags: the stable version, with Frama-C sources,
`framac/frama-c:XX.Y` (where `XX.Y` is Frama-C's latest stable release);
the development version `framac/frama-c:dev`, a daily snapshot of Frama-C's
repository; `framac/frama-c-gui:XX.Y` and `framac/frama-c-gui:dev`, which are
equivalent versions with the Frama-C GUI (running a GUI in Docker is not
trivial, but with Singularity or other tools it is doable); and the
`framac/frama-c:dev-stripped` image, which has a much smaller footprint
but lacks source files and several non-essential components.
Still, if you need an older Frama-C version for performing quick tests, these
images might help.
# Comparing the output of Frama-C 5.0 (Boron) and Frama-C 23.1 (Vanadium), more than 10 years later
For nostalgia's sake, let us compare the result of running
the old Value analysis on this code, which has a signed overflow, versus
running a recent version of the Eva plug-in:
```c
int abs(int i) {
if (i < 0) return -i; // no good: signed overflow for INT_MIN
else return i;
}
int main() {
int a = (int)((unsigned)(((unsigned)-1)/2)+1); // results in INT_MIN
int r = abs(a);
return r;
}
```
With `framac/frama-c:5.0-stripped`, running
`frama-c -val -val-signed-overflow-alarms`<sup>1</sup>:
<sup>1</sup> *In the Boron release, the option to enable signed overflows
was considered *experimental* and had to be manually enabled.
```
[kernel] preprocessing with "gcc -C -E -I. abs.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
[value] computing for function abs <-main.
Called from abs.c:8.
abs.c:2:[kernel] warning: signed overflow, should be between -2147483648 and 2147483647: assert
(((-0x7FFFFFFF-1)
≤ -i)
(-i ≤
2147483647));
[value] Recording results for abs
abs.c:2:[kernel] warning: non termination detected in function abs
[value] Done for function abs
[value] Recording results for main
abs.c:9:[kernel] warning: non termination detected in function main
[value] done for function main
[dominators] computing for function abs
[dominators] done for function abs
[value] ====== VALUES COMPUTED ======
[value] Values for function abs:
NON TERMINATING FUNCTION
[value] Values for function main:
NON TERMINATING FUNCTION
```
With the latest development version, post-23.1 (Vanadium), running `frama-c -eva`:
```
[kernel] Parsing abs.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] abs.c:2: Warning: signed overflow. assert -i ≤ 2147483647;
[eva] done for function main
[eva] abs.c:2: assertion 'Eva,signed_overflow' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function abs:
NON TERMINATING FUNCTION
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
2 functions analyzed (out of 2): 100% coverage.
In these functions, 5 statements reached (out of 11): 45% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
1 alarm generated by the analysis:
1 integer overflow
1 of them is a sure alarm (invalid status).
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
```
As we can see, some messages survived more than 10 years.
Others were slightly reworded; and a new features are entirely new, such as
the analysis summary.
# Conclusion
Given C's pitfalls and slow evolution, it is likely that such warnings will
remain necessary yet for years to come. At least, maybe in 10 years we will
be able to get rid of
[signed magnitude representation for integers](http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2218.htm),
and avoid this message when using option `-no-warn-signed-overflow`:
```
[eva:signed-overflow] abs.c:2: Warning: 2's complement assumed for overflow
```
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