mirror of
https://github.com/nim-lang/Nim.git
synced 2025-12-29 01:14:41 +00:00
9ffec79300
* code cleanups and feature additions * added basic test and koch/CI integration * make it build on Unix * DrNim: now buildable on Unix, only takes 10 minutes, enjoy * added basic documentation for DrNim which can also be seen as the RFC we're following * drnim: change the build setup so that drnim.exe ends up in bin/ * makes simple floating point ranges work * added basic float range check * drnim: teach Z3 about Nim's range types plus code refactoring * drnim: make unsigned numbers work * added and fixed index checking under setLen * first implementation of .ensures, .invariant and .assume (.requires still missing and so is proc type compatibility checking * drnim: .requires checking implemented * drnim: implemented .ensures properly * more impressive test involving min() * drnim: check for proc type compatibility and base method compatibility wrt .requires and .ensures * testament: support for 'pattern <directory> * koch: uses new <directory> feature of testament * drnim: added tiny musings about 'old' * Make testament work with old SSL versions * koch: add support for 'koch drnim -d:release' * drnim: preparations for the param.old notation
44 lines
893 B
Nim
44 lines
893 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
|
|
|
|
{.pop.}
|
|
|
|
p([1, 2, 3], [4, 5])
|