Frama-C news and ideas

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

Tag - nitrogen

Entries feed - Comments feed

Tuesday, March 27 2012

Overflow alarms vs informative messages about 2's complement

A privately sent question may deserve a quick blog post.

Context

The example is as below:

int x, y, s;

main(){
  x = Frama_C_interval(0, 2000000000);
  y = 1000000000;
  s = x + y;
  Frama_C_dump_each();
}

Sorry for all the zeroes. There are nine of them in each large constant, so that the program is flirting with the limits of 32-bit 2's complement integers. Frama-C's value analysis with default options finds the following to say:

$ frama-c -val share/builtin.c o.c
...
o.c:6:[value] warning: 2's complement assumed for overflow
o.c:6:[value] assigning non deterministic value for the first time
[value] DUMPING STATE of file o.c line 7
        x ∈ [0..2000000000]
        y ∈ {1000000000}
        s ∈ [--..--]

There is an option, -val-signed-overflow-alarms, to change the behavior of the value analysis with respect to integer overflows:

$ frama-c -val -val-signed-overflow-alarms share/builtin.c o.c
...
o.c:6:[kernel] warning: Signed overflow. assert x+y ≤ 2147483647LL;
o.c:6:[value] assigning non deterministic value for the first time
[value] DUMPING STATE of file o.c line 7
        x ∈ [0..2000000000]
        y ∈ {1000000000}
        s ∈ [1000000000..2147483647]

The warning with the first command was introduced in Nitrogen, and this post therefore is in a way part of the series describing new features in Nitrogen.

The new warning, “2's complement assumed for overflow”, is emitted in exactly the same circumstances the alarm “assert x+y ≤ 2147483647LL” would have been emitted if option -val-signed-overflow-alarms had been used.

Question and answer

The question is whether the warnings obtained in each case, “2's complement assumed for overflow” and “Signed overflow. assert x+y ≤ 2147483647LL” respectively, mean the same thing. The answer is that no, they don't. The consequences of the differences between them can be seen in the values computed for variable s after the overflow.

  1. The warning “2's complement assumed for overflow” is a gentle reminder that the value analysis is unable to establish an overflow does not happen at line 6. The value analysis is, the message kindly informs, going to assume that the overflow, if it happens at all, happens on purpose. The programmer may for instance have read that blog post in addition to this one, and use the appropriate options to force GCC to give 2's complement results on signed overflows. The message considered here is informative only. The user should is expected to react with “ah, yes, that's right, my program overflows on purpose here” and go on with some of eir analysis. Only two billion and one values can actually be obtained as a result of this 2's complement addition, [-2147483648..-1294967296] ∪ [1000000000..2147483647], but since the value analysis can only represent large sets of integers as a single interval, the end result is that all int values appear to be possible values for variable s.
  2. The warning “Signed overflow. assert x+y ≤ 2147483647LL” contains the word “assert”. It is an alarm. The user should do something about it, and in this case, the user should realize ey is trying to prove that there are no undefined signed overflows in a program that really contains undefined signed overflows. Something is seriously wrong in the target program! The value analysis wants to be as precise as possible for the rest of the program, so without deciding of the status of the alarm, it assumes for the rest of the propagation that it was false. If the overflow alarm is false, then s is guaranteed to be in the range [1000000000..2147483647]. This is a subset of the values that are possible with 2's complement addition. Now, the value analysis also reserves the right to reduce, after the alarm, the values for variable x to the range [0..1147483647], since these are the only values that do not cause an undefined overflow. It does not take advantage of this information at this level for now, but a future version will. The reasoning here is the same as the reasoning in Q1 and Q2 in the Frequently Asked Questions section of the manual.


It may seem strange that in the second case, the value analysis does not affirm more strongly that there is a definite problem with some of the values in the user-specified Frama_C_interval(0, 2000000000) range for variable x, but that's not what it is optimized for. It is optimized for verifying that there aren't any issues, not so much for reliably telling the user what original inputs cause the issues. User expertise or alternative techniques must take up from there. Think of the range [0..2000000000] for x as the result of previous computations, without it being known whether the interval is so wide because the values can really happen with user-specified inputs, or because of earlier over-approximations.


Stéphane Duprat, Florent Kirchner and Philippe Herrmann proofread this post.

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.

Monday, December 5 2011

Formidable colleagues, patchlevels and new features in Nitrogen

My colleagues are formidable. Over the last few days, three of them fixed four bugs in my code. And one of the fixes was a simple, obviously correct fix for the bug previously discussed here.


In celebration of these terrific colleagues, here is a new patchset for Nitrogen 20111001, patchlevel 2. It replaces patchlevel 1. I have tested it as thoroughly as the previous one, that is, I didn't even check if it applied cleanly to the Nitrogen tarball.


Finally, with the aforementioned bugfix out the door, it is time to boast about another new feature available in Nitrogen: string constants. String constants are now properly treated as read-only: the program is not supposed to write there. If it does, an alarm is emitted, and for the sake of precision when analyzing the rest of the program, it is assumed that the write did not take place in the string constant. If the pointer could also point somewhere writable, then the write is assumed to take place there instead. If the pointer was only pointing to read-only or otherwise unwritable locations, the propagation ends for that state.

If this seems a bit abstract, here is the same example as before, revisited:

char *p = "foo";
char c;
char s = 'F';

void f(int u)
{
  if (u) p = &c;
  *p = s;
}

Treating f as the entry point of the program, the analyzer doesn't know what values may be passed for the argument u. Just before assigning to *p, it assumes that p may point to c or inside "foo", but as the program tries to write to *p, it warns that p had better point somewhere writable, and since the user will of course make sure of that, it then knows that p points to c, and since p was pointing to c, it also knows that c contains 'F' at the end of the function:

...
bl.c:8:[kernel] warning: out of bounds write. assert \valid(p);
...
[value] Values at end of function f:
          p ∈ {{ &c }}
          c ∈ {70}

One of the next steps will be to transform the "p points somewhere writable" condition before the assignment into "u is non-null" as a pre-condition of function f(), using weakest pre-condition computation. Quite a lot of effort remains before this works. For one thing, the value analysis does not yet distinguish between "valid for reading" and "valid for writing" in the ACSL predicates it annotates the program with (although it makes the distinction in the log messages).

Speaking of string constants, I should also mention that the value analysis in Nitrogen emits a warning for "foo" == "foo". I already boasted about that here, but Nitrogen wasn't released at the time.


This post was brought to you thanks to the formidableness of Philippe Herrmann, Virgile Prevosto, and Boris Yakobowski.

Wednesday, November 23 2011

Fixes in Nitrogen's value analysis

Speaking of bug fixes, here is what a proper post-release patch looks like. This patch fixes five issues identified since Nitrogen was released. I have not tested the patch itself (I have not even tried applying it to the original tarball) — this is where you come in, dear reader. Let's call it "patchlevel 1" for now. It may be given more official status if no additional fixes are incorporated. Or perhaps not even then.

It is recommended for users who build from source and for packagers, who always manage their own sets of patches anyway. It contains only fixes for confirmed issues, and each fix is simple enough to be an obviously uniform improvement.


Boris Yakobowski contributed several of the fixes in patchlevel 1. To be fair, he may, in the course of his excellent and broad-scoped developments, have originally contributed some of the bugs being fixed, too.

Bug in Nitrogen's value analysis

In the course of restructuring the value analysis, I noticed a difference in some regression tests. The "after" version had some new warnings that weren't in the "before" version. After further investigation, it turned out that displaying the warnings was correct, and that the "before" version was unsound.

This soundness bug is particularly hard to reproduce even if you know it's there. I am still pondering whether to back-port the fix to the released Nitrogen version, because it basically means back-porting the internal architecture change, not the kind of small, obviously uniform improvements I like to release as post-release patches.


The bug appears in this example program:

char *p = "foo";
char c;
char s = 'F';

void f(int u)
{
  if (u) p = &c;
  *p = s;
}

Here is the entire output of an analysis with Nitrogen:

$ ~/nitrogen-20111001/bin/toplevel.opt -val t.c -main f
[kernel] preprocessing with "gcc -C -E -I.  t.c"
[value] Analyzing a complete application starting at f
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        p ∈ {{ &"foo" }}
        c ∈ {0}
        s ∈ {70}
[value] Recording results for f
[value] done for function f
[value] ====== VALUES COMPUTED ======
[value] Values for function f:
          p ∈ {{ &c }}
          c ∈ {70}

Here is the output of today's version. Can you spot the difference?

[kernel] preprocessing with "gcc -C -E -I.  t.c"
[value] Analyzing a complete application starting at f
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        p ∈ {{ &"foo" }}
        c ∈ {0}
        s ∈ {70}
t.c:8:[kernel] warning: out of bounds write. assert \valid(p);
[value] Recording results for f
[value] done for function f
[value] ====== VALUES COMPUTED ======
[value] Values for function f:
          p ∈ {{ &c }}
          c ∈ {70}

In Nitrogen, the value analysis sees that it is illegal for p to point to literal string "foo" since *p is used for writing. It deduces that the value of p can only be &c, and that the assignment of 'F' (ASCII code 70) can only take place in c, and that the final value of c is therefore necessarily 70, but it forgets to emit the alarm stating that p must not point to "foo". The current development version follows the same reasoning but remembers to emit the alarm.

In order to observe this bug, it is necessary to shape *p = ...; as an lvalue to lvalue assignment (*p = 'F'; does not produce the bug). Lvalue to lvalue assignments are handled specially in order to enable precise results on struct assignments and memcpy() of addresses.

Besides, the bug only occurs with pointers to literal strings or to arrays that are automatically allocated when the analysis entry point takes pointers in arguments — but the creation of these arrays is not documented in enough detail for users to realize there is a bug in this case.

Lastly, if in the example p pointed only inside the literal string, then the illegal write access would be even more obvious (since there would be no location for the write to happen) and the alarm would be emitted (that is, the bug wouldn't occur).

Industrial users with SVN read access can simply use today's version, where the bug is fixed.


Sometimes I wish the value analysis only propagated intervals. It would have simpler bugs then.

Monday, October 17 2011

Features in Frama-C Nitrogen, part 1

Here is a series of posts that highlight interesting features in the recently released Frama-C Nitrogen 20111001. There is new functionality in Nitrogen, that we hope will entice both existing and prospective users. Other improvements yet will only have meaning for existing users. I will start off with two items from this second category.

Nitrogen compiles with OCaml 3.10.2.

The only non-optional dependency for compiling Nitrogen is an OCaml compiler. But which one? Despite a now long history, the OCaml language is still evolving relatively rapidly. We have never been happier with our choice of an implementation language: it is evolving in a direction that suits us, and it is evolving conservatively (compare Perl 6, PHP 5, Python 3, …). On the other hand, Frama-C is large and contains tricky code; the plug-in architecture with dynamic loading in general on the one hand, and the hash-consing programming technique on the other hand, are only two examples. It is large enough and tricky enough to reveal many of the subtle difference between any two versions of the OCaml compiler.

Nitrogen compiles with the latest version of OCaml, of course. That's 3.12.1 at the time of this writing. We already know that it won't compile as-is with the future OCaml 3.13 (a patch will be released in due time). Similarly, support for older versions has to be gained, version by version. If you have only written medium-sized OCaml programs, you could easily underestimate the difficulty of this. I was lucky enough not to have to deal with it much during this cycle, but some of my colleagues had to. It always is a struggle. Sometimes the equivalent of #define/#if constructs from C pre-processing would help, but this is not idiomatic in OCaml. Again, the only non-optional dependency for compiling Nitrogen is an OCaml compiler, so we won't use fine solutions such as Cppo.


For Windows and Mac OS X, OCaml is not part of the operating system, so we ship the version we like together with the binary package (if we make one). With Unix, the issues are different: there are too many flavors for us to distribute binaries, but there are efficient package systems and distributions to painlessly bring in required dependencies. Often, Frama-C itself is packaged in binary or source form as part of these distributions, thanks to the work of many volunteers. It may take some time for packages to be created for Nitrogen, and some users do not want to wait. Linus Token, for instance, may rely on a computer he bought two years ago. Frama-C works fine on two-years old computers, as seen in the next section. Linus installed his Unix distribution of choice when he bought his computer, and now he expects Frama-C's sources to compile with the OCaml version from his distribution (OCaml programmers can be expected to have the latest OCaml compiler installed from its own sources, but Linus is not an OCaml programmer). The Unix distribution installed two years ago was on average 3 months old at that time, and it may have been frozen for stability 3 months before being released. For Linus, Frama-C has to compile with a 2.5-year-old compiler. And then there are industrial users who like to trail a little bit on the Linux front, but at the same time want all the latest Frama-C features. For Nitrogen, we chose to retain compatibility with OCaml 3.10.2, released in February 2008, and all OCaml versions released since.

The value analysis is up to four times faster on realistic examples

The second Nitrogen feature I want to highlight today the value analysis' speed. Here is a quick and dirty comparison for programs that could already be analyzed with Carbon. There are new alarms and precision improvements in Nitrogen, but I made sure that in this comparison, the two versions were doing the same amount of work.

For this comparison, I did not cherry-pick benchmarks. I looked for programs of varying sizes in the archives of the blog, and used the three that came first, having decided in advance that I wouldn't dismiss any results I didn't like. Each analysis was run three times, and the median time was kept. This is on a Core 2 mobile processor, and the frequency is pinned at 1.5GHz through CoolBook. In plain English, the timings are for an oldish but not antiquated notebook.

The options I used were:

-slevel 1000 -val count.c
-slevel 10000 -val -no-results -cpp-command "gcc -C -E -m32 -Dprintf=Frama_C_show_each" sha1.c
-val -slevel 1000 -slevel-function main:0 *.c -cpp-command "gcc -m32 -C -E -I. "

The programs count.c and sha1.c came from this post. For sha1.c I had to disable the endianness detection code, implemented with a switch, to put the Carbon and Nitrogen versions on an equal footing. With the Carbon version, there used to be a difficult choice to make in presence of switch, remember? I could also have used option -simplify-cfg for the Carbon execution, but then the analyzers would not have been analyzing exactly the same program. The Skein-256 example is the verification that an arbitrary number of calls to Skein_256_Update(..., 80) never cause a run-time error, using Josh Ko's instrumentation.

                             count.c     sha1.c      Skein-256

Carbon                       0m0.491s    0m2.862s    1m10.201s
Nitrogen without Zarith      0m0.410s    0m1.724s    0m37.782s
Nitrogen with Zarith         0m0.313s    0m0.962s    0m16.700s

Total speed-up                 1.5          3            4

How did the value analysis improve so much overall? As exemplified by the timings with and without Zarith, this is the result of many small enhancements and refinements at all levels.

Conclusion

As promised, the two features described here are only worth noting for faithful users. It only matters that Frama-C compiles with OCaml 3.10.2 if you intend to compile it at all, and you only care that it is much faster than before if you were already using it. Even so, some of the existing users may not notice them. This is the kind of feature that I like, because it does not complicate the user interface —the value analysis benchmarks above use the same options and produce the same results— and improves the software nonetheless. Existing users and people who try Frama-C for the first time with Nitrogen will both have a better time of it thanks to the effort spent on the two points described in this post, and on tens of others, big and small, some of which I hope will receive their own minute of spotlight in this series. I have been forced to allude to one other small improvement, a better treatment of switch in the value analysis, that I like even better because it removes the need to learn one option.