| FazBrowse GitHub Viewer | Trending | | Home |
| Tools: [Download Repo ZIP] [Original HTTPS Page] |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
@@ -51,19 +51,27 @@ predicate allocExprOrIndirect(Expr alloc, string kind) { | |||
| 51 | 51 | ) | |
| 52 | 52 | } | |
| 53 | 53 | ||
| 54 | + /** | ||
| 55 | + * Holds if `v` is assigned value `e`, and `e` is not known to be `0`. | ||
| 56 | + */ | ||
| 57 | + private predicate nonNullGlobalAssignment(Variable v, Expr e) { | ||
| 58 | + not v instanceof LocalScopeVariable and | ||
| 59 | + v.getAnAssignedValue() = e and | ||
| 60 | + not e.getValue().toInt() = 0 | ||
| 61 | + } | ||
| 62 | + | ||
| 54 | 63 | /** | |
| 55 | 64 | * Holds if `v` is a non-local variable which is assigned only with allocations of | |
| 56 | 65 | * type `kind` (it may also be assigned with NULL). | |
| 57 | 66 | */ | |
| 58 | 67 | private predicate allocReachesVariable(Variable v, Expr alloc, string kind) { | |
| 59 | - not v instanceof LocalScopeVariable and | ||
| 60 | 68 | exists(Expr mid | | |
| 61 | - v.getAnAssignedValue() = mid and | ||
| 69 | + nonNullGlobalAssignment(v, mid) and | ||
| 62 | 70 | allocReaches(mid, alloc, kind) | |
| 63 | - ) and forall(Expr mid | | ||
| 64 | - v.getAnAssignedValue() = mid | | ||
| 65 | - allocReaches(mid, _, kind) or | ||
| 66 | - mid.getValue().toInt() = 0 // NULL | ||
| 71 | + ) and | ||
| 72 | + forall(Expr mid | | ||
| 73 | + nonNullGlobalAssignment(v, mid) | | ||
| 74 | + allocReaches(mid, _, kind) | ||
| 67 | 75 | ) | |
| 68 | 76 | } | |
| 69 | 77 | ||
| Back | FazBrowse Home | New Git URL |
0 commit comments