Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Tag - obviously-terminates

Entries feed - Comments feed

Tuesday, August 21 2012

Participating in the RERS 2012 competition: liveness questions

This third installment discusses the diagnosis of liveness properties of particular C programs, using Frama-C's value analysis, for the RERS 2012 competition.


[Note added in September 2012: the diagnostic found for the example in this post disagrees with the diagnostic found later and sent to the competition organizers. I am unable to reproduce the result obtained here. Perhaps it was obtain with a version of Frama-C that had a bug.]

Liveness properties 101

Here is another extract of two properties found in the property list attached to Problem 1 in the competition:

(G ! oW)
output W does never occur
----------------------------------------

(F oW)
output W occurs eventually

To tell you how unaccustomed to temporal properties I am, I first read the second formula as a negation of the first one. There are redundancies in the lists of formulas to evaluate, and I thought this was one more of them. It is of course not the case: (F oW) is not the negation of (G ! oW).

(G ! oW) says that there is no execution path that leads to W being output; the negation of that is that there is at least one such execution path. By contrast, (F oW) expresses that all execution paths have a W being output at some point, a much stronger property.


Indeed, (F oW), expressing that a state in which W is output is eventually reached, is a typical liveness property. Checking this kind of property is at odds with traditional abstract interpretation practices, where the analysis is considered done when a fixpoint has been reached: the fixpoint does not tell whether all executions eventually leave the loop. It only tells what is guaranteed for those executions that leave the loop.

Semi-solution: a simple program transformation

Please bear with me and consider the simple modification of Problem1.c below, applied on top of the previous instrumentation:

--- Problem1.c	2012-08-08 10:15:00.000000000 +0200
+++ Problem1_terminate_at_W.c	2012-08-21 17:00:38.000000000 +0200
@@ -1,9 +1,8 @@
 void assert(int x)
 {
   if (!x)
     {
-      Frama_C_show_each_assert_reached();
       /*@ assert \false; */
     }
 }
 
@@ -594,6 +593,8 @@
 
         // operate eca engine
         output = calculate_output(input);
 
+	// continue only if output not W yet
+	/*@ assert output != w ; */
     }
 }

We remove the user message in our assert() function because we want to temporarily forget about assertions. Besides, by instrumenting the main loop, we make the program stop when the output is W.

You should be able to convince yourself that the modified program terminates if and only if the original program does not admit any infinite execution that never outputs W (for any infinite sequence of values assigned to variable input).


Earlier posts (1, 2) in this blog pointed out how Frama-C's value analysis could be made to forget that it was an abstract interpreter, and verify the termination of programs.

Application

Since everything is ready for this particular property of Problem1.c, let us run the verification. The command to prove that the program terminates is as follows:

$ frama-c -val -obviously-terminates -no-val-show-progress Problem1_terminate_at_W.c
...
[value] Semantic level unrolling superposing up to 400 states
[value] done for function main
[value] ====== VALUES COMPUTED ======

We should have used a timeout, because the analysis fails to terminate when the analyzer is unable to prove that the target program terminate. Nevertheless, we were lucky, the target program terminates, the analyzer is able to verify that the program terminates, and we can conclude that there are no infinite executions of the original Program1.c that fail to emit W.

Assertions and consequences on liveness properties

The previous section only tells us that there is no infinite execution that does not emit W. Depending on the organizers' intentions, this may or may not answer the question of whether (F oW) holds.

It still depends whether you count an execution that reaches one of the assert(0); in the program as, well, an execution. If it count as an execution to which the formula should apply, then an execution that does not emit W and terminates on such an assert(0); certainly does not eventually output W.

There is an argument to say that it shouldn't count, however: although it is impossible to understand what these programs are supposed to do, assertions usually characterize illegal behaviors. Perhaps the LTL formulas are to be evaluated only on the legal, infinite behaviors of the system?

In the latter case, we are done: (F oW) holds because W is eventually emitted in all legal executions. In the former case, the additional question is whether an original assert(0); is reached before W is output, which is a simple reachability question on the instrumented Problem1_terminate_at_W.c. The answer is then that (F oW) does not hold, because there are plenty of assert(0); calls that are reached without W having been emitted.


We e-mailed the organizers and they said it was the first, simpler case. Only infinite executions need be taken into account for evaluating LTL formulas, and interrupted executions can be ignored. Our answer for the formula (F oW) of Problem 1 in the competition is therefore that the property holds.

Proving that something does not eventually happen

In the first part of the post, we set out to prove that the liveness property (F oW) was true. Verifying that the property is false requires a different approach. With the toolset provided by Frama-C, I only see the scheme below. We reduce the problem to the seemingly harder but actually easier problem of computing the maximum number of iterations before W is emitted.

  1. Obtain the number N of reachable states for the system by running the value analysis on the original program.
  2. Instrument the program, as previously making execution terminate when W is emitted, and also maintaining a transition counter (incremented at each iteration of the loop).
  3. Using sound and complete propagation on the instrumented program, either reach a fixpoint (with a finite bound computed for the counter) or find an execution with N+1 transitions that does not emit W. The former case means that the program eventually emits W. The latter that, in the transition graph, there is a reachable cycle along which W is not emitted, and therefore an infinite execution that does not output W.


This technique likely gets pretty heavy in practice. Adding a counter that may go up to N+1 to a system that already has N states can probably cause the new system to have of the order of N² states. This segues into at least one, perhaps two more blog posts, to answer the questions “what is the value analysis actually doing when it is applied on these questions?”, “how much work would it be to do the same thing closer to the metal, executing the C function as compiled instead of laboriously interpreting it?”, and “why don't we make a C model checker while we are at it?”

Friday, June 8 2012

To finish on termination

Enthusiastic reactions to the previous post about verifying the termination of a C program with Frama-C's value analysis lead me to write this post-scriptum.

On detecting both termination and non-termination

The scheme I outlined in the previous post can only confirm the termination of the program. If the program does not terminate, the analysis method I outlined runs indefinitely. I recommended to use a timeout and to interpret reaching the timeout as the answer “I don't know”. Off-line, a colleague complained about this behavior.


This colleague was, of course, being facetious. Frama-C's value analysis, when used normally (without option -obviously-terminates) is already a sound detector of non-termination. Consider the program below:

unsigned char u = 1;

int main(){
  while (u)
    {
      u = u + 14;
    }
  return u;
}

If you can get Frama-C's value analysis to print that the function is a “NON TERMINATING FUNCTION”, it means that the function is guaranteed not to have any defined terminating executions (to put it simply, the function is guaranteed not to terminate). In this case, it is easy:

$ frama-c -val t4.c
[value] Values at end of function main:
          NON TERMINATING FUNCTION

The values displayed as possible at the end of the function are sound over-approximations of the values that are possible in real (defined) executions. When the value analysis says that there are no possible values, you can trust that there are no real executions that reach the end of the function.


For more difficult cases, I recommend option -slevel to improve the chances that the analyzer will detect non-termination. The guarantees are the same as before: if the value analysis says “NON TERMINATING FUNCTION”, no real execution reaches the end of the function. If it describes possible values for variables at the end of the function, it mean that, because of over-approximations, it doesn't know whether the end of the function is reached at all.


unsigned char u;

int main(){
  while (u * u != 17)
    {
      u = u + 1;
    }
  return u;
}

The program above looks for a number whose square is 17. With the default settings, the value analysis is unable to decide whether the program terminates or not:

$ frama-c -val t5.c
...
[value] Values at end of function main:
          u ∈ [--..--]
          __retres ∈ [0..255]


Let us now analyze the program more precisely with option -slevel 300:

~ $ frama-c -slevel 300 -val t5.c
...
[value] Values at end of function main:
          NON TERMINATING FUNCTION

That's better: the above result means that the value analysis can guarantee that the program will keep searching for an unsigned char whose square is 17 until the end of the world.


To summarize:

  • If you want to verify non-termination, you can hope to do so with Frama-C's value analysis in normal mode.
  • If you want to verify termination, you can hope to do so with Frama-C's value analysis with option -obviously-terminate.
  • If you don't know whether the target program terminates or not and you want to chance to detect both, then you can launch both frama-c -val and frama-c -obviously-terminates -val in parallel and see whether one of them is able to conclude one way or the other.
  • If you want an analyzer that always tells in finite time whether a given program terminates or not, and although a C program without dynamic allocation is not exactly similar to a Turing machine, you may be asking too much.

On the Collatz conjecture

An expedient shortcut, when trying to explain undecidability to non-computer scientists, is to encode a famous, well-researched mathematical conjecture into a computer program, ideally one with a large monetary prize attached to it. It works well as an intuitive explanation of the difficulty of saying anything about the dynamic behavior of arbitrary programs. The argument is that if it was easy to tell whether an arbitrary program does something or the other, some mathematician would have taken the opportunity to become famous, and possibly rich, by encoding the conjecture as a computer program and analyzing this program. This is, of course, an informal meta-argument. Perhaps all mathematicians are stupid; we don't know about that. But I find this explanation of undecidability works better than any other I have tried.

A long time ago, I was using Fermat's last theorem for the above purpose. When it started to be considered satisfactorily proved, I switched to Goldbach's conjecture. But Goldbach's conjecture requires enumerating prime numbers. To encode it into the simplest possible program for the purpose of an informal explanation, one needs to write at least a function that recognizes a prime number, and explain that this is good enough to encode the conjecture into a program.


All this time, I should have been using the Collatz conjecture (that you may also know as “Syracuse problem”). My facetious colleagues reminded me of this in the comments to the previous post.


Let us humor these colleagues:

unsigned long long x;

unsigned long long input();

main(){
  x = input();
  while (x > 1)
    {
      if (x%2 == 0) x = x/2; else x = 3*x + 1;
    }
}

Trying to prove termination:

$ frama-c -obviously-terminates -val syracuse.c 
...
[value] Semantic level unrolling superposing up to 53600 states
[value] Semantic level unrolling superposing up to 53700 states
[value] Semantic level unrolling superposing up to 53800 states
^C[kernel] User Interruption (Ctrl-C)

Trying to prove non-termination:

$ frama-c -slevel 44444 -val syracuse.c
...
[value] Values at end of function main:
          x ∈ {0; 1}
          __retres ∈ {0}

Both attempts failed. Ah well, at least we tried.

Thursday, June 7 2012

Verifying the termination of programs with value analysis option -obviously-terminates

What's old about option -obviously-terminates

Option -obviously-terminates is a value analysis option, new in Nitrogen, with some of the same effects as using an infinite slevel. This option also disables fixpoint detection and the statement-wise memorisation of analysis results.

I briefly described this option in a previous post, in section “Trying to improve results by doing things differently”. This option was originally intended for the interpretation of Csmith-generated programs. Csmith-generated programs are executable, and it is possible to make sure that they terminate by simply letting them run for a few milliseconds. Once it is known that a Csmith-generated program terminates, then the value analysis' job interpreting the program is much easier with option -obviously-terminates. This option tells it not to waste time looking for a fixpoint, since in this case, it could only find one if the program looped, which we know it doesn't.

What's new about option -obviously-terminates

Option -obviously-terminates can be used to verify the termination of C programs.


Used this way, it is sound—when it diagnoses the program as terminating, then the program always terminates. It is not complete: it may fail to answer for programs that terminate. Actually, it always either diagnoses the program as terminating or fails to answer: it must be used with a timeout. It tries to make the program terminate until the timeout, and the timeout being reached must be interpreted as the answer “I don't know”.

This new insight into an existing option is as new for me as it is for you: I genuinely did not realize that this option could do this until this morning's shower. I was close, because in the previously linked blog post, I had written:

“[Option -obviously-terminates] makes [the value analysis] loop forever on C programs that loop forever — like an interpreter does”

But it did not occur to me to contrapose the above statement until I tried a few examples into the web interface for sett, Germán Vidal's symbolic execution-based termination tool. I am extremely thankful to him for making this web interface available.

Examples

Here is a first example with non-obvious termination:

char x, y;

main()
{
  x = input();
  y = input();
  while (x>0 && y>0)
    {
      if (input() == 1)
	{
	  x = x - 1;
	  y = input();
	}
      else
	y = y - 1;
    }
}

Note the use of the (signed) type char for variables x and y, to limit combinatorial explosion.

$ frama-c -obviously-terminates -val t1.c

[kernel] preprocessing with "gcc -C -E -I.  t1.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        x ∈ {0}
        y ∈ {0}
[value] computing for function input <- main.
        Called from t1.c:5.
...
   (several seconds here)
...
[value] Semantic level unrolling superposing up to 48100 states
...
[value] Done for function input
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======

Frama-C's value analysis with option -obviously-terminates was able to finish its analysis of this example. This means that the program terminates for all possible integers returned by input().


Another example:

char x, y;

main()
{
  x = input();
  y = input();

  while (x>0 && y>0)
    {
      // Frama_C_dump_each();
      if (input())
        {
          x = x - 1;
          y = x;
        }
      else
        {
          x = y - 2;
          y = x + 1;
        }
    }
}
$ frama-c -obviously-terminates -val t2.c 
...
[value] ====== VALUES COMPUTED ======

This means once again that the program terminates for all possible integers returned by input().

I couldn't believe how fast the analysis of this second example was, so I inserted the Frama_C_dump_each(); call. If you uncomment it, you can see the abstract states that have been considered during the analysis, and how they become smaller and smaller, until it becomes obvious that all execution paths eventually exit the loop.


The two above examples were taken from the sett website. They can be found, in the sett input language syntax, inside the PDF description of the tool. Here is a third example invented by me:


char x;

main(){
  x = input();
  while (x > 0)
    {
      Frama_C_dump_each();
      if (x > 11)
        x = x - 12;
      else
        x = x + 1;
    }
}

Again, frama-c -obviously-terminates -val shows the termination of this program. It is very quick in this case since the interval for variable x is initially reduced by slices of 12 values at a time, and then the value analysis carefully analyzes the tricky part, which takes most of the time.

Monday, March 12 2012

Minimizing the number of alarms emitted by the value analysis

This blog post describes for the first time some options that became available in Nitrogen, continuing this series. This post also offers a benchmark, but the results of this benchmark cannot be reproduced with Nitrogen. They should be reproducible with the next version of Frama-C.

Alarms, false alarms and redundant alarms

Frama-C's value analysis computes two results for further processing: values and alarms. In this post, we assume that the list of alarms is what the user is interested in. That is, eir objective is to obtain a list of conditions (alarms) that ey will only need to check never happens in order to be assured that the program is defined. Defined in the sense of the value analysis, that is. Understandably, the user would like to spend as little time and memory as possible to obtain this list. However, because human or computation time is going to be spend further processing each alarm, ey would like the list to be as short as possible. Ey is willing to spend some extra time and memory shortening the list, within reason.

The user still wants the list to be exhaustive. One valid way to shorten the list is to remove false alarms from it, if the extra time and memory can be used to determine that some of the alarms are false alarms. Another alarm that can validly be removed from the list is a redundant alarm that cannot happen as long as another, previous alarm is verified not to happen first. One example of a redundant alarm that the value analysis cannot easily remove by itself is provided in the manual:

int A, B;
void main(int x, int y)
{
  A = 100 / (x * y);
  B = 333 % x;
}

This example assumes signed overflows give 2's complement results (and should not be considered as dangerous). With these settings, the value analysis emits two alarms:

$ frama-c -val div.c
div.c:4: ... assert (int)(x*y) ≢ 0;
div.c:5: ... assert x ≢ 0;

The alarm at line 5 is redundant with the alarm at line 4. The alarm at line 5 could theoretically be removed, because if x*y is non-nil, then x is guaranteed to be non-nil too (and the reasoning applies even if “x*y is non-nil” is taken to mean that the product is non-nil modulo 2^32).

Unrelated exercise for the motivated reader: through command-line options and program annotations, guide the analyzer so that it only emits the alarm at line 4, without making any assumption that it wasn't making in the original analysis.

Example: a string manipulation function

This example was provided by some of my colleagues. More on that later. For now, it suffices to say that the set-up is perfect: the command frama-c -metrics gd_full_bad.c shows that it only needs Frama_C_interval(), provided in a file builtin.c with Frama-C. The analysis runs with frama-c -val .../share/frama-c/builtin.c gd_full_bad.c.

The basic approach

The green belt user, having read the tutorial, knows that after checking that eir analysis project does not call any missing functions and doing an imprecise analysis, if said imprecise analysis is fast enough, ey has the option to run the analysis again with option -slevel for a chance to obtain more precise results. More precise results means fewer alarms, so a good first benchmark is to measure the effects of various values of -slevel on analysis time and how many alarms these analysis seconds gain us.

for i in 0 10 100 1000 10000 100000 
do
  /usr/bin/time ~/ppc/bin/toplevel.opt ... -slevel $i > log_slevel_$i 2> time_slevel_$i
done

The table below gives for each value used for the -slevel option, the analysis time and the number of alarms emitted.

slevel    alarms    time(s)
     0     13         0.61
    10     13         0.62
   100     13         1.0
  1000     12         6.0
 10000      9       105
100000      1       441

The single alarm that remains even with -slevel 100000 is at a line preceded by the comment /* BAD */ in the source code. With the information implicitly carried in the name of the file, we can assume this one to be a true alarm, intended to be found and that will not go away with any value of -slevel. Further assuming there are no other bugs to be found in this code (which is what the value analysis claims), one alarm is the optimal result and it is found in exchange for a wait of a little bit more than 7 minutes. The same alarm is present in the lists of 9, 12 or 13 alarms found with the other values of -slevel, together with, respectively, 8, 11 and 12 false or redundant alarms.

Improving results with advanced options

Improving results by doing less

The advanced user knows that when you are not interested in the “values” component of the value analysis' results, you can save a sometimes significant amount of time by instructing the analyzer not to save them for you. An hitherto less documented option is -no-val-show-progress, that similarly saves the analyzer the bother of printing progression messages, for when no-one is going to read them.

slevel    alarms    time(s)
     0     13         0.45
    10     13         0.47
   100     13         0.9
  1000     12         5.5
 10000      9        97
100000      1       439

As you can see, the difference is almost lost in the noise, which means that I should probably compute confidence intervals and/or boot some of the other users out of the server I am using for this informal comparison. But I'm not going to. The shell commands in this blog post are, among other things, so that I can run everything again at a quieter time.

Improving results by doing more

Little-known option -remove-redundant-alarms takes some time at the end of the analysis to detect whether some alarms are syntactically identical to prior alarms. If the variables involved in both alarms were left unmodified by the program in-between, the latter alarm is identified as redundant and erased from the alarms database.

Detecting whether some alarms are redundant in this manner requires the “values” part of the value analysis' results to resolve pointers, so if we use this option, we cannot use option -no-results. For the good that one did us, option -remove-redundant-alarms is worth a try.

Note that -remove-redundant-alarms does not retroactively remove emitted alarms from the log. You can obtain the filtered list programmatically, by looking for it in the GUI, or with option -print.

Running again the previous tests with option -remove-redundant-alarms, the difference in computation time is lost in the noise when compared to the timings without option -no-results. For this negligible price, one assertion is removed from the list of 13 obtained with values 0, 10 and 100 of option -slevel.

One assertion removed as redundant may not seem like much, but it means that for this particular example, if you are starting from -slevel 0 and are willing to spend just enough additional resources to go from 13 to 12 alarms, you are better off investing in -remove-redundant-alarms, that will take 0.10s to get you there, than in -slevel 1000, that will require 5s of additional computation time for the same result.


$ ~/ppc/bin/toplevel.opt ... -remove-redundant-alarms -print > lrm
$ ~/ppc/bin/toplevel.opt ... -print > lpl
$ diff -u lpl lrm
--- lpl	2012-03-12 21:38:54.000000000 +0100
+++ lrm	2012-03-12 21:38:49.000000000 +0100
@@ -42,6 +42,9 @@
 gd_full_bad.c:143:[value] Assertion got status unknown.
 gd_full_bad.c:46:[value] warning: 2's complement assumed for overflow
 [value] done for function main
+[from] Computing for function search
+[from] Done for function search
+[scope] [rm_asserts] removing 1 assertion(s)
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function Frama_C_interval:
           Frama_C_entropy_source ∈ [--..--]
@@ -293,9 +296,6 @@
           }
         }
         len = 1;
-        /*@ assert \valid{Here}(string+next);
-              // synthesized
-           */
         byte = (int)((unsigned char)*(string + next));
         if (byte < 0xC0) { len = 1; }
         else {

As this log-level comparison shows, with option -remove-redundant-alarms, the same alarms are initially found (there are no differences there). With the option, Frama-C works harder (lines starting with + indicate work that was done only when the option was present) and removes one alarm from the final printout (lines starting with -). The assertion \valid{Here}(string+next) was found to be redundant with a previous, syntactically identical assertion.

Trying to improve results by doing things differently

Experiments with using the value analysis as a C interpreter, that have been alluded to in this blog, led to the introduction in Nitrogen of value analysis option -obviously-terminates. I have previously described this option as emulating infinite slevel and disabling fixpoint detection, which is one way to see what it does. More accurately, it disables the detection of previously-propagated states. Whereas one may associate fixpoint detection with the analysis of loops, the detection of previously seen states normally occurs even outside of loops. It is this detection that is disabled by the option, and therefore, the option also influences the analysis of loop-free programs.

The “obviously” in the name of the option is a reminder that it will only be useful for programs that terminate very obviously. Fixpoint detection and widening are the two techniques through which the value analysis terminates when analyzing programs that themselves do not terminate, or do not clearly terminate. Option -obviously-terminates disables both. The consequence is that the analyzer can loop forever. When it is used to turn the value analysis into a C interpreter, it makes it loop forever on C programs that loop forever — like an interpreter does. If the option is used outside “interpreter constraints” (for instance, if there is initial imprecision on some inputs or if some functions are missing), then the value analysis may even loop while analyzing programs that in reality terminate for all their inputs. Lastly, one should keep in mind that it is not enough that the termination of the analyzed program is obvious for the user. It needs to be obvious for the analyzer.

An example

Consider the following loop-free program:

int x, y, z, t, u, ...;

int main (int c, char **v)
  x = c & 1;
  if (x)
    x = 1;
  else
    x = 2;
  y = x + 1;
  z = y;
  t = z - 1;
  u = t;
  ...

When this program is analyzed with -slevel 2 or more, the analyzer spends its time, at each statement, wondering whether the state coming from the initial then branch has been propagated into something identical to the state coming from the initial else branch. This kind of test can be expensive, especially when programs with many execution paths are analyzed with high values of -slevel. Also, on this program or a program similar to this one, making the test at each statement is a complete waste of time: two states will never be found to be identical, if only because the state coming from the then and else branches always have different values for variable x.

Option -obviously-terminates disables these time-wasting tests, and makes the analysis of a program like this one much faster.

Another, very slightly different example

Consider the following following variation of the previous program:

int x, y, z, t, u, ...;

int main (int c, char **v)
  x = c & 1;
  if (x)
    x = 1;
  else
    x = 1;
  y = x + 1;
  z = y;
  t = z - 1;
  u = t;
  ...

When analyzing this program without option -obviously-terminates, the analyzer immediately recognizes that the states corresponding to the two branches of the if are the same state, and merges them into one. Once a single state is left, no further expensive inclusion tests are necessary, and the analyzer zips through the rest of the program at maximal speed.

With option -obviously-terminates, on the other hand, the analyzer never tests whether the two branches can be merged. It basically does twice the work, propagating each state in duplicate through the rest of the program.

Concluding on option -obviously-terminates

When you are thinking of using option -obviously-terminates:

  1. You should wonder whether the analysis will then terminate.
  2. You should wonder whether the analyzed program is more like the first example or more like the second one. If it is more like the first one, you may hope that the analysis, with what will effectively amount to infinite slevel, will be faster.

When an analysis with option -obviously-terminates finishes, the results obtained are functionally equivalent to results that would have been obtained with an infinite slevel.

What about the current benchmark?

The value -slevel 100000, the highest one we used, also amounts to offering infinite slevel to the analyzer: the analyzer does not consume the 100000 allowed states, using up only about half. One last data point we can therefore obtain is the analysis time with option -obviously-terminates in replacement of -slevel 100000.

It turns out that the benchmark is more like the second example above: the analysis takes longer with option -obviously-terminates, about half an hour instead of 7 minutes. The option makes having states propagated through the same program point comparatively cheap, because inclusion does not have to be tested. On the other hand, because inclusion is not tested, some program points see 500000 states propagated through them, or about ten times more than the maximum when option -obviously-terminates is not used. Although each of them is less expensive to handle, having to deal with ten times as many states hurts the bottom line for this benchmark.

Well, it was worth trying. Unsurprisingly, after the half hour is elapsed, the same single alarm is found as in the -slevel 100000 analysis.

Conclusion

The number of options available in the Frama-C platform can be a little bit overwhelming. It is for a good reason that the value analysis tutorial emphasizes option -slevel and this option only. On the example from this post, it does not hurt very much only to know about this one: it allows you to obtain the optimal result, and you do not seem to be penalized by more than a few seconds for not remembering all the other ones.

Unfortunately, the example in this post is only one example, and in special cases, it may be necessary to have more than one string to one's bow.