next steps for guarded data flow analysis

2 files changed, 64 insertions, 1 deletions

diff --git a/tests/reject/tcheckedfield1.nim b/tests/reject/tcheckedfield1.nim
new file mode 100644
index 000000000..f74a8b76d
--- /dev/null
+++ b/tests/reject/tcheckedfield1.nim
@@ -0,0 +1,60 @@
+discard """
+  errormsg: "cannot prove that field 's' is accessible"
+  line:54
+"""
+
+import strutils
+
+{.warning[ProveField]: on.}
+
+type
+  TNodeKind = enum
+    nkBinary, nkTernary, nkStr
+  PNode = ref TNode not nil
+  TNode = object
+    case k: TNodeKind
+    of nkBinary, nkTernary: a, b: PNode
+    of nkStr: s: string
+    
+  PList = ref object
+    data: string
+    next: PList
+
+proc getData(x: PList not nil) =
+  echo x.data
+
+var head: PList
+
+proc processList() =
+  var it = head
+  while it != nil:
+    getData(it)
+    it = it.next
+
+proc toString2(x: PNode): string =
+  if x.k < nkStr:
+    toString2(x.a) & " " & toString2(x.b)
+  else:
+    x.s
+
+proc toString(x: PNode): string =
+  case x.k
+  of nkTernary, nkBinary:
+    toString(x.a) & " " & toString(x.b)
+  of nkStr:
+    x.s
+
+proc toString3(x: PNode): string =
+  if x.k <= nkBinary:
+    toString3(x.a) & " " & toString3(x.b)
+  else:
+    x.s # x.k in {nkStr}  --> fact:  not (x.k <= nkBinary)
+
+proc p() =
+  var x: PNode = PNode(k: nkStr, s: "abc")
+  
+  let y = x
+  if not y.isNil:
+    echo toString(y), " ", toString2(y)
+
+p()
diff --git a/tests/reject/tnotnil1.nim b/tests/reject/tnotnil1.nim
index 3535bbd63..222c77376 100644
--- a/tests/reject/tnotnil1.nim
+++ b/tests/reject/tnotnil1.nim
@@ -1,6 +1,6 @@
 discard """
   errormsg: "'y' is provably nil"
-  line:22
+  line:25
 """
 
 import strutils
@@ -15,6 +15,9 @@ proc q(x: pointer not nil) =
 
 proc p() =
   var x: pointer
+  if not x.isNil:
+    q(x)
+  
   let y = x
   if not y.isNil:
     q(y)