mirror of
https://github.com/nim-lang/Nim.git
synced 2025-12-28 08:54:53 +00:00
3a2697dd73
* drnim: tiny progress * refactoring complete * drnim: prove .ensures annotations * Moved code around to avoid code duplication * drnim: first implementation of the 'old' property * drnim: be precise about the assignment statement * first implementation of --assumeUnique * progress on forall/exists handling
52 lines
990 B
Nim
52 lines
990 B
Nim
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])
|