Gabriel Kerneis wrote:
> On Wed, Aug 26, 2009 at 11:30:47PM +0200, Roberto Bagnara wrote:
>> a = ++(*p);
>
> Are you sure the behavior of this line is defined in C? I don't how it
> could be incorrect to translate it to:
> (*p)++;
> a = *p;
> (which is precisely what CIL does).
Hi Gabriel.
Let us consider this example:
$ cat /tmp/bug2.c
#include <stdio.h>
int main() {
struct l {
struct l** next;
} s[4];
struct l* a;
struct l* p[4];
struct l* old;
p[0] = s;
p[0]->next = &p[0];
old = (*p[0]->next);
a = ((*p[0]->next) += 1);
if (old + 1 != a)
printf("bug!\n");
return 0;
}
$ gcc -W -Wall -pedantic /tmp/bug2.c
$ a.out
$ cilly /tmp/bug2.c
gcc -D_GNUCC -E -DCIL=1 /tmp/bug2.c -o /tmp/cil-5WCc5w5N.i
/usr/local/distrib/cil/obj/x86_LINUX/cilly.asm.exe --out
/tmp/cil-11qSEAG2.cil.c /tmp/cil-5WCc5w5N.i
gcc -D_GNUCC -E /tmp/cil-11qSEAG2.cil.c -o /tmp/cil-l3XsLPCk.cil.i
gcc -D_GNUCC -c -o /tmp/cil-dUTI4nQq.o /tmp/cil-l3XsLPCk.cil.i
gcc -D_GNUCC -o a.out /tmp/cil-dUTI4nQq.o
$ a.out
bug!
$
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.
All the best,
Roberto
P.S. I just noticed that Frama-C uses a modified version
of CIL: perhaps they have fixed these problems.
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagn...@cs.unipr.it
------------------------------------------------------------------------------
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
