Download first.c.

Command-line use

The command-line version of Frama-C has few dependencies so that there is little that may have gone wrong there. Still, here are a few tests:

$ frama-c -val first.c -slevel 10
[kernel] preprocessing with "gcc -C -E -I.  first.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        S ∈ {0}
        T[0..4] ∈ {0}
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
          S ∈ {10}
          T[0] ∈ {0}
           [1] ∈ {1}
           [2] ∈ {3}
           [3] ∈ {6}
           [4] ∈ {10}
          i ∈ {5}
          p ∈ {{ &T + {20} }}
$ frama-c first.c -quiet -slice-wr i -then-on 'Slicing export' -print
first.c:8:[kernel] warning: out of bounds write. assert \valid(tmp);
first.c:8:[value] warning: 2's complement assumed for overflow
/* Generated by Frama-C */
void main(void)
  int i;
  i = 0;
  while (i < 5) { i ++; }

If you obtain the same output when typing each of these two commands, the command-line version of Frama-C is doing fine.

Graphical user interface

Type the command:

$ frama-c-gui -val first.c -slevel 10

After a few seconds (but it may take longer the first time), you should obtain a window looking like:


If, in the middle panel, you click on the occurrence of variable S inside the loop body, you should then see: