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 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:

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¹:

¹ 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, and avoid this message when using option -no-warn-signed-overflow:

[eva:signed-overflow] abs.c:2: Warning: 2's complement assumed for overflow