--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on January 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Value Analysis] multi state propagation



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.