added an .assert pragma and mentioned the pragmas in the changelog
This commit is contained in:
parent
df8e0e7f0c
commit
d01fca974d
4 changed files with 8 additions and 4 deletions
|
|
@ -169,6 +169,10 @@ echo f
|
||||||
enabling things like lvalue references, see `byaddr.byaddr`
|
enabling things like lvalue references, see `byaddr.byaddr`
|
||||||
|
|
||||||
- `macro pragmas` can now be used in type sections.
|
- `macro pragmas` can now be used in type sections.
|
||||||
|
- 5 new pragmas were added to Nim in order to make the upcoming tooling more
|
||||||
|
convenient to use. Nim compiler checks these pragmas for syntax but otherwise
|
||||||
|
ignores them. The pragmas are `requires`, `ensures`, `assume`, `assert`, `invariant`.
|
||||||
|
|
||||||
|
|
||||||
## Language changes
|
## Language changes
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1176,7 +1176,7 @@ proc singlePragma(c: PContext, sym: PSym, n: PNode, i: var int,
|
||||||
if sym == nil: invalidPragma(c, it)
|
if sym == nil: invalidPragma(c, it)
|
||||||
else: sym.flags.incl sfUsed
|
else: sym.flags.incl sfUsed
|
||||||
of wLiftLocals: discard
|
of wLiftLocals: discard
|
||||||
of wRequires, wInvariant, wAssume:
|
of wRequires, wInvariant, wAssume, wAssert:
|
||||||
pragmaProposition(c, it)
|
pragmaProposition(c, it)
|
||||||
of wEnsures:
|
of wEnsures:
|
||||||
pragmaEnsures(c, it)
|
pragmaEnsures(c, it)
|
||||||
|
|
|
||||||
|
|
@ -1030,7 +1030,7 @@ proc track(tracked: PEffects, n: PNode) =
|
||||||
when defined(drnim):
|
when defined(drnim):
|
||||||
if pragma == wAssume:
|
if pragma == wAssume:
|
||||||
addFact(tracked.guards, pragmaList[i][1])
|
addFact(tracked.guards, pragmaList[i][1])
|
||||||
elif pragma == wInvariant:
|
elif pragma == wInvariant or pragma == wAssert:
|
||||||
if prove(tracked, pragmaList[i][1]):
|
if prove(tracked, pragmaList[i][1]):
|
||||||
addFact(tracked.guards, pragmaList[i][1])
|
addFact(tracked.guards, pragmaList[i][1])
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -54,7 +54,7 @@ type
|
||||||
wNonReloadable, wExecuteOnReload,
|
wNonReloadable, wExecuteOnReload,
|
||||||
wAssertions, wPatterns, wTrMacros, wSinkInference, wWarnings,
|
wAssertions, wPatterns, wTrMacros, wSinkInference, wWarnings,
|
||||||
wHints, wOptimization, wRaises, wWrites, wReads, wSize, wEffects, wTags,
|
wHints, wOptimization, wRaises, wWrites, wReads, wSize, wEffects, wTags,
|
||||||
wRequires, wEnsures, wInvariant, wAssume,
|
wRequires, wEnsures, wInvariant, wAssume, wAssert,
|
||||||
wDeadCodeElimUnused, # deprecated, dead code elim always happens
|
wDeadCodeElimUnused, # deprecated, dead code elim always happens
|
||||||
wSafecode, wPackage, wNoForward, wReorder, wNoRewrite, wNoDestroy,
|
wSafecode, wPackage, wNoForward, wReorder, wNoRewrite, wNoDestroy,
|
||||||
wPragma,
|
wPragma,
|
||||||
|
|
@ -143,7 +143,7 @@ const
|
||||||
|
|
||||||
"assertions", "patterns", "trmacros", "sinkinference", "warnings", "hints",
|
"assertions", "patterns", "trmacros", "sinkinference", "warnings", "hints",
|
||||||
"optimization", "raises", "writes", "reads", "size", "effects", "tags",
|
"optimization", "raises", "writes", "reads", "size", "effects", "tags",
|
||||||
"requires", "ensures", "invariant", "assume",
|
"requires", "ensures", "invariant", "assume", "assert",
|
||||||
"deadcodeelim", # deprecated, dead code elim always happens
|
"deadcodeelim", # deprecated, dead code elim always happens
|
||||||
"safecode", "package", "noforward", "reorder", "norewrite", "nodestroy",
|
"safecode", "package", "noforward", "reorder", "norewrite", "nodestroy",
|
||||||
"pragma",
|
"pragma",
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue