--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on January 2013 ---
Hello List, I am trying to use the value analysis to have precise results on an example that is similar to this very simplified one : ------------------------------------------ //@ assigns \nothing; unsigned int ext (void); int N = 0; unsigned int local (void) { unsigned int f = ext (); if (f) N++; Frama_C_dump_each (); return f; } int main (void) { unsigned int f = local (); Frama_C_dump_each (); if (f) N--; //@ assert N == 0; return 0; } ------------------------------------------ Using : frama-c -val test.c -slevel 100 The first Frama_C_dump_each (in 'local') shows that the context is split in two parts : [value] DUMPING STATE of file test.c line 13 N ? {1} f ? [1..4294967295] =END OF DUMP== [value] DUMPING STATE of file test.c line 13 N ? {0} f ? {0} =END OF DUMP== what is exactly what I expected. But unfortunately, it seems that the two states are then merged before being propagated to the 'main' as shown by the second Frama_C_dump_each (in 'main') : [value] DUMPING STATE of file test.c line 19 N ? {0; 1} f ? [--..--] =END OF DUMP== I then get : test.c:20:[value] assigning non deterministic value for the first time test.c:21:[value] Assertion got status unknown. I managed to get the precise result with : $ frama-c -val test.c -slevel 100 -val-split-return-function local:0 [value] DUMPING STATE of file test.c line 19 N ? {0} f ? {0} =END OF DUMP== [value] DUMPING STATE of file test.c line 19 N ? {1} f ? [1..4294967295] =END OF DUMP== test.c:21:[value] Assertion got status valid. But it doesn't scale when the call stack is deeper. What would be great is to be able to specify "something" about either 'ext' (like : ensures f == 0 || f > 0;) or in 'local' (like: ensures (f == 0 && N == \old(N)) || (f > 0 && N == \old(N)+1);) and to tell the analysis that we would like to propagate the two states. Is it possible to do something like that ? Did I missed something ? Thanks in advance for your help. -- Anne.