Hi,
Roberto Bagnara a écrit :
> Generally speaking, I wonder how the program verification
> tools based on CIL cope with this kind of problems (this
> is not the first such problem I report on the list).
> And this is relatively independent from the fact that the
> source program has fully defined behavior or not: how can
> tools that are meant to ensure the program has defined
> behavior be based on a frontend that does not preserve
> the relevant features of the analyzed program? That is
> what surprises me.
> P.S. I just noticed that Frama-C uses a modified version
> of CIL: perhaps they have fixed these problems.
Indeed Frama-C is meant to be able to handle the case you mention. We
had to preserve some informations about the possibly undefined
behaviours coming from the original code. They one has to prove that
these behaviours never occur.
frama-c -print t.c
outputs:
===========
int main(void)
{
struct l s[4] ;
struct l *a ;
struct l *p[4] ;
struct l *old ;
int __retres ;
p[0] = s;
(p[0])->next = p;
old = *((p[0])->next);
{ /*unspecified sequence*/ (*((p[0])->next)) ++; a = *((p[0])->next); }
if (old + 1 != a) { printf((char const *)"bug!\n"); }
__retres = 0;
return (__retres);
}
=========
The internal AST looks like this:
{ /*unspecified sequence*/
/*sid:5*/
(*((p[0])->next)) ++;
/*effects: *((p[0])->next) <- (p[0])->next, p[0], p*/
/*sid:6*/
a = *((p[0])->next);
/*effects: a <- */
}
Then your code is correct if the effects are disjoint.
Note that we do not intend to guess the behaviour of the different
compilers nor to pretty-print a code with the "same undefinedness" as
the original one.
But you are warned that your code is not ISO compliant and that a
compiler might do anything it wants with it (including terminating the
program).
Some corner cases of undefined behaviours are not yet handled by Frama-C.
Hope this helps,
--
| Benjamin Monate | mailto:benjamin.mon...@cea.fr |
| Head of Software Safety Lab. CEA-LIST/DRT/DTSI/SOL/LSL |
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
