Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
83 lines (69 sloc) 1.34 KB
//
// Correct redundant test
//
// Target: Linux, Generic
// Copyright: 2012 - LIP6/INRIA
// License: Licensed under ISC. See LICENSE or http://www.isc.org/software/license
// Author: Julia Lawall <Julia.Lawall@lip6.fr>
// URL: http://coccinelle.lip6.fr/
// URL: http://coccinellery.org/
// Copyright: (C) 2009 Gilles Muller, Julia Lawall, INRIA, DIKU. GPLv2.
@r exists@
local idexpression x;
expression E;
position p1,p2;
@@
if (x@p1 == NULL || ...) { ... when forall
return ...; }
... when != \(x=E\|x--\|x++\|--x\|++x\|x-=E\|x+=E\|x|=E\|x&=E\)
when != &x
when any
(
x@p2 == NULL
|
x@p2 != NULL
)
// another path to the test that is not through p1?
@s exists@
local idexpression r.x;
position r.p1,r.p2;
@@
... when != x@p1
(
x@p2 == NULL
|
x@p2 != NULL
)
// another path to the test from p1?
@t exists@
local idexpression x;
position r.p1,r.p2;
@@
if (x@p1 == NULL || ...) { ... x@p2 ... when any
return ...; }
// another path to the test containing an assignment?
@u exists@
local idexpression x;
expression E;
position r.p1,r.p2;
@@
if (x@p1 == NULL || ...) { ... when forall
return ...; }
...
\(x=E\|x--\|x++\|--x\|++x\|x-=E\|x+=E\|x|=E\|x&=E\|&x\)
... when != x@p1
when any
(
x@p2 == NULL
|
x@p2 != NULL
)
@depends on !s && !t && !u expression@
position r.p2;
expression x;
@@
(
* x@p2 != NULL || ...
|
* x@p2 == NULL
)