diff options
| author | Andreas Rumpf <rumpf_a@web.de> | 2020-03-31 22:54:48 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-31 22:54:48 +0200 |
| commit | 9ffec79300e35fe100c657317eff21e9b8779d8b (patch) | |
| tree | 81008f0c1165fd24c22a9d0166306b4e4d55bd0a /lib | |
| parent | dd44701728f6bc9e6e6b4b2548b707221a075758 (diff) | |
| download | Nim-9ffec79300e35fe100c657317eff21e9b8779d8b.tar.gz | |
DrNim (Nim compiler with Z3 integration) (#13743)
* 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
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/std/logic.nim | 10 | ||||
| -rw-r--r-- | lib/system/strmantle.nim | 8 |
2 files changed, 17 insertions, 1 deletions
diff --git a/lib/std/logic.nim b/lib/std/logic.nim new file mode 100644 index 000000000..3cc871a6e --- /dev/null +++ b/lib/std/logic.nim @@ -0,0 +1,10 @@ +## This module provides further logic operators like 'forall' and 'exists' +## They are only supported in ``.ensures`` etc pragmas. + +proc `->`*(a, b: bool): bool {.magic: "Implies".} +proc `<->`*(a, b: bool): bool {.magic: "Iff".} + +proc forall*(args: varargs[untyped]): bool {.magic: "Forall".} +proc exists*(args: varargs[untyped]): bool {.magic: "Exists".} + +proc old*[T](x: T): T {.magic: "Old".} diff --git a/lib/system/strmantle.nim b/lib/system/strmantle.nim index a111ec563..c3ac5fc1b 100644 --- a/lib/system/strmantle.nim +++ b/lib/system/strmantle.nim @@ -115,6 +115,9 @@ const 1e10, 1e11, 1e12, 1e13, 1e14, 1e15, 1e16, 1e17, 1e18, 1e19, 1e20, 1e21, 1e22] +when defined(nimHasInvariant): + {.push staticBoundChecks: off.} + proc nimParseBiggestFloat(s: string, number: var BiggestFloat, start = 0): int {.compilerproc.} = # This routine attempt to parse float that can parsed quickly. @@ -236,7 +239,7 @@ proc nimParseBiggestFloat(s: string, number: var BiggestFloat, # if exponent is greater try to fit extra exponent above 22 by multiplying # integer part is there is space left. let slop = 15 - kdigits - fdigits - if absExponent <= 22 + slop and not expNegative: + if absExponent <= 22 + slop and not expNegative: number = sign * integer.float * powtens[slop] * powtens[absExponent-slop] return i - start @@ -274,6 +277,9 @@ proc nimParseBiggestFloat(s: string, number: var BiggestFloat, else: number = c_strtod(t, nil) +when defined(nimHasInvariant): + {.pop.} # staticBoundChecks + proc nimInt64ToStr(x: int64): string {.compilerRtl.} = result = newStringOfCap(sizeof(x)*4) result.addInt x |