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

_posts/2021-10-15-old-frama-c-docker-images.md

+---
+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
+```