diff options
| author | Araq <rumpf_a@web.de> | 2014-09-21 18:39:00 +0200 |
|---|---|---|
| committer | Araq <rumpf_a@web.de> | 2014-09-21 18:39:00 +0200 |
| commit | 7916b1f9aa93fca368afda8b18396230ac7f338c (patch) | |
| tree | 04072aeee4ae211b91c088a7267455b82daf9787 /compiler/guards.nim | |
| parent | 4800acf6ab92799316b270c991b6e8c01454608f (diff) | |
| download | Nim-7916b1f9aa93fca368afda8b18396230ac7f338c.tar.gz | |
implemented 'guard' annotation
Diffstat (limited to 'compiler/guards.nim')
| -rw-r--r-- | compiler/guards.nim | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/compiler/guards.nim b/compiler/guards.nim index 05128f409..cd0aaf296 100644 --- a/compiler/guards.nim +++ b/compiler/guards.nim @@ -838,6 +838,22 @@ proc addAsgnFact*(m: var TModel, key, value: PNode) = fact.sons[2] = value m.add fact +proc sameSubexprs*(m: TModel; a, b: PNode): bool = + # This should be used to check whether two *path expressions* refer to the + # same memory location according to 'm'. This is tricky: + # lock a[i].guard: + # ... + # access a[i].guarded + # + # Here a[i] is the same as a[i] iff 'i' and 'a' are not changed via '...'. + # However, nil checking requires exactly the same mechanism! But for now + # we simply use sameTree and live with the unsoundness of the analysis. + var check = newNodeI(nkCall, a.info, 3) + check.sons[0] = newSymNode(opEq) + check.sons[1] = a + check.sons[2] = b + result = m.doesImply(check) == impYes + proc addCaseBranchFacts*(m: var TModel, n: PNode, i: int) = let branch = n.sons[i] if branch.kind == nkOfBranch: |