summary refs log tree commit diff stats
path: root/drnim/tests/tsetlen_invalidates.nim
diff options
context:
space:
mode:
Diffstat (limited to 'drnim/tests/tsetlen_invalidates.nim')
-rw-r--r--drnim/tests/tsetlen_invalidates.nim26
1 files changed, 26 insertions, 0 deletions
diff --git a/drnim/tests/tsetlen_invalidates.nim b/drnim/tests/tsetlen_invalidates.nim
new file mode 100644
index 000000000..f3e595744
--- /dev/null
+++ b/drnim/tests/tsetlen_invalidates.nim
@@ -0,0 +1,26 @@
+discard """
+  nimout: '''tsetlen_invalidates.nim(12, 10) Warning: BEGIN [User]
+tsetlen_invalidates.nim(18, 12) Warning: cannot prove: 0 <= len(a) + -1; counter example: a`1.len -> 0
+a.len -> 1 [IndexCheck]
+tsetlen_invalidates.nim(26, 10) Warning: END [User]
+'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+{.warning: "BEGIN".}
+
+proc p() =
+  var a = newSeq[int](3)
+  if a.len > 0:
+    a.setLen 0
+    echo a[0]
+
+  if a.len > 0:
+    echo a[0]
+
+{.pop.}
+
+p()
+{.warning: "END".}