|
@@ -20,7 +20,11 @@ expression E;
|
|
|
position p1;
|
|
position p1;
|
|
|
@@
|
|
@@
|
|
|
|
|
|
|
|
-kfree@p1(E)
|
|
|
|
|
|
|
+(
|
|
|
|
|
+* kfree@p1(E)
|
|
|
|
|
+|
|
|
|
|
|
+* kzfree@p1(E)
|
|
|
|
|
+)
|
|
|
|
|
|
|
|
@print expression@
|
|
@print expression@
|
|
|
constant char [] c;
|
|
constant char [] c;
|
|
@@ -60,7 +64,11 @@ position ok;
|
|
|
@@
|
|
@@
|
|
|
|
|
|
|
|
while (1) { ...
|
|
while (1) { ...
|
|
|
- kfree@ok(E)
|
|
|
|
|
|
|
+(
|
|
|
|
|
+* kfree@ok(E)
|
|
|
|
|
+|
|
|
|
|
|
+* kzfree@ok(E)
|
|
|
|
|
+)
|
|
|
... when != break;
|
|
... when != break;
|
|
|
when != goto l;
|
|
when != goto l;
|
|
|
when forall
|
|
when forall
|
|
@@ -74,7 +82,11 @@ statement S;
|
|
|
position free.p1!=loop.ok,p2!={print.p,sz.p};
|
|
position free.p1!=loop.ok,p2!={print.p,sz.p};
|
|
|
@@
|
|
@@
|
|
|
|
|
|
|
|
-kfree@p1(E,...)
|
|
|
|
|
|
|
+(
|
|
|
|
|
+* kfree@p1(E,...)
|
|
|
|
|
+|
|
|
|
|
|
+* kzfree@p1(E,...)
|
|
|
|
|
+)
|
|
|
...
|
|
...
|
|
|
(
|
|
(
|
|
|
iter(...,subE,...) S // no use
|
|
iter(...,subE,...) S // no use
|