5 files changed, 184 insertions, 0 deletions
diff --git a/drnim/tests/config.nims b/drnim/tests/config.nims
new file mode 100644
index 000000000..346b0b4e6
--- /dev/null
+++ b/drnim/tests/config.nims
@@ -0,0 +1,10 @@
+switch("path", "$nim/testament/lib") # so we can `import stdtest/foo` in this dir
+
+## prevent common user config settings to interfere with testament expectations
+## Indifidual tests can override this if needed to test for these options.
+switch("colors", "off")
+switch("filenames", "canonical")
+switch("excessiveStackTrace", "off")
+
+# we only want to check the marked parts in the tests:
+switch("staticBoundChecks", "off")
diff --git a/drnim/tests/tbasic_array_index.nim b/drnim/tests/tbasic_array_index.nim
new file mode 100644
index 000000000..8ae019e78
--- /dev/null
+++ b/drnim/tests/tbasic_array_index.nim
@@ -0,0 +1,51 @@
+discard """
+  nimout: '''tbasic_array_index.nim(26, 17) Warning: cannot prove: 0 <= len(a) - 4; counter example: a.len -> 0 [IndexCheck]
+tbasic_array_index.nim(32, 5) Warning: cannot prove: 4.0 <= 1.0 [IndexCheck]
+tbasic_array_index.nim(38, 36) Warning: cannot prove: a <= 10'u32; counter example: a -> #x000000000000000b
+'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+
+proc takeNat(n: Natural) =
+  discard
+
+proc p(a, b: openArray[int]) =
+  if a.len > 0:
+    echo a[0]
+
+  for i in 0..a.len-8:
+    #{.invariant: i < a.len.}
+    echo a[i]
+
+  for i in 0..min(a.len, b.len)-1:
+    echo a[i], " ", b[i]
+
+  takeNat(a.len - 4)
+
+proc r(x: range[0.0..1.0]) = echo x
+
+proc sum() =
+  r 1.0
+  r 4.0
+
+proc ru(x: range[1u32..10u32]) = echo x
+
+proc xu(a: uint) =
+  if a >= 4u:
+    let chunk = range[1u32..10u32](a)
+    ru chunk
+
+proc parse(s: string) =
+  var i = 0
+
+  while i < s.len and s[i] != 'a':
+    inc i
+
+parse("abc")
+
+{.pop.}
+
+p([1, 2, 3], [4, 5])
diff --git a/drnim/tests/tensures.nim b/drnim/tests/tensures.nim
new file mode 100644
index 000000000..f4e8f84e6
--- /dev/null
+++ b/drnim/tests/tensures.nim
@@ -0,0 +1,74 @@
+discard """
+  nimout: '''tensures.nim(18, 10) Warning: BEGIN [User]
+tensures.nim(27, 5) Warning: cannot prove:
+0 < n [IndexCheck]
+tensures.nim(47, 17) Warning: cannot prove: a < 4; counter example: y -> 2
+a`2 -> 4
+a`1 -> 3
+a -> 2 [IndexCheck]
+tensures.nim(69, 17) Warning: cannot prove: a < 4; counter example: y -> 2
+a`1 -> 4
+a -> 2 [IndexCheck]
+tensures.nim(73, 10) Warning: END [User]'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+import std/logic
+{.push staticBoundChecks: defined(nimDrNim).}
+{.warning: "BEGIN".}
+
+proc fac(n: int) {.requires: n > 0.} =
+  discard
+
+proc g(): int {.ensures: result > 0.} =
+  result = 10
+
+fac 7 # fine
+fac -45 # wrong
+
+fac g() # fine
+
+proc main =
+  var x = g()
+  fac x
+
+main()
+
+proc myinc(x: var int) {.ensures: x == old(x)+1.} =
+  inc x
+  {.assume: old(x)+1 == x.}
+
+proc mainB(y: int) =
+  var a = y
+  if a < 3:
+    myinc a
+    {.assert: a < 4.}
+    myinc a
+    {.assert: a < 4.} # now this is wrong!
+
+mainB(3)
+
+proc a(yy, z: int) {.requires: (yy - z) > 6.} = discard
+# 'requires' must be weaker (or equal)
+# 'ensures'  must be stronger (or equal)
+
+# a 'is weaker than' b iff  b -> a
+# a 'is stronger than' b iff a -> b
+# --> We can use Z3 to compute whether 'var x: T = q' is valid
+
+type
+  F = proc (yy, z3: int) {.requires: z3 < 5 and z3 > -5 and yy > 10.}
+
+var
+  x: F = a # valid?
+
+proc testAsgn(y: int) =
+  var a = y
+  if a < 3:
+    a = a + 2
+    {.assert: a < 4.}
+
+testAsgn(3)
+
+{.warning: "END".}
+{.pop.}
diff --git a/drnim/tests/tphi.nim b/drnim/tests/tphi.nim
new file mode 100644
index 000000000..7ff49f4dc
--- /dev/null
+++ b/drnim/tests/tphi.nim
@@ -0,0 +1,23 @@
+discard """
+  nimout: '''tphi.nim(9, 10) Warning: BEGIN [User]
+tphi.nim(22, 10) Warning: END [User]'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+import std/logic
+{.push staticBoundChecks: defined(nimDrNim).}
+{.warning: "BEGIN".}
+
+proc testAsgn(y: int) =
+  var a = y
+  if a > 0:
+    if a > 3:
+      a = a + 2
+    else:
+      a = a + 1
+    {.assert: a > 1.}
+
+testAsgn(3)
+
+{.warning: "END".}
+{.pop.}
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".}