Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] [Value Analysis] multi state propagation
  • From: anne.pacalet at free.fr (Anne Pacalet)
  • Date: Tue, 29 Jan 2013 09:33:42 +0100
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.