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.nim22
1 files changed, 22 insertions, 0 deletions
diff --git a/drnim/tests/tsetlen_invalidates.nim b/drnim/tests/tsetlen_invalidates.nim
new file mode 100644
index 000000000..03620af10
--- /dev/null
+++ b/drnim/tests/tsetlen_invalidates.nim
@@ -0,0 +1,22 @@
+discard """
+  nimout: '''
+tsetlen_invalidates.nim(15, 12) Warning: cannot prove: 0 <= len(a) + -1; counter example: a.len -> 0 [IndexCheck]
+'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+
+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()