You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
text.dfy(2,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
1
+
text.dfy(2,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'.
Copy file name to clipboardExpand all lines: latest/DafnyRef/Attributes.md
+11-4Lines changed: 11 additions & 4 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -393,12 +393,15 @@ Print effects are enforced only with `--track-print-effects`.
393
393
`{:priority N}` assigns a positive priority 'N' to a method or function to control the order
394
394
in which methods or functions are verified (default: N = 1).
395
395
396
-
### 11.2.14. `{:rlimit}` {#sec-rlimit}
396
+
### 11.2.14. `{:resource_limit}` and `{:rlimit}` {#sec-rlimit}
397
397
398
-
`{:rlimit N}` limits the verifier resource usage to verify the method or function at `N * 1000`.
399
-
This is the per-method equivalent of the command-line flag `/rlimit:N`.
398
+
`{:resource_limit N}` limits the verifier resource usage to verify the method or function to `N`.
399
+
400
+
This is the per-method equivalent of the command-line flag `/rlimit:N` or `--resource-limit N`.
400
401
If using [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) as well, the limit will be set for each assertion.
401
402
403
+
The attribute `{:rlimit N}` is also available, and limits the verifier resource usage to verify the method or function to `N * 1000`. This version is deprecated, however.
404
+
402
405
To give orders of magnitude about resource usage, here is a list of examples indicating how many resources are used to verify each method:
403
406
404
407
* 8K resource usage
@@ -848,6 +851,10 @@ method Test()
848
851
849
852
The success message is optional but is recommended if errorMessage is set.
850
853
854
+
### 11.4.6. `{:contradiction}`
855
+
856
+
Silences warnings about this assertion being involved in a proof using contradictory assumptions when `--warn-contradictory-assumptions` is enabled. This allows clear identification of intentional proofs by contradiction.
`autoRevealDependencies` makes all functions not explicitly labelled as opaque to be opaque but reveals them automatically in scopes which do not have `{:autoRevealDependencies false}`.
106
78
`opaque` means functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof.
107
79
108
-
/generalTraits:<value>
109
-
legacy (default) - Every trait implicitly extends 'object', and thus is a reference type. Only traits and reference types can extend traits.
110
-
datatype - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits.
111
-
full - (don't use; not yet completely supported) A trait is a reference type only if it or one of its ancestor traits is 'object'. Any type with members can extend traits.
112
-
113
-
/ntitrace:<value>
114
-
0 (default) - Don't print debug information for the new type system.
115
-
1 - Print debug information for the new type system.
116
-
117
80
/readsClausesOnMethods:<value>
118
81
0 (default) - Reads clauses on methods are forbidden.
119
82
1 - Reads clauses on methods are permitted (with a default of 'reads *').
Prevents a warning from being generated for axioms, such as assume statements and functions or methods without a body, that don't have an {:axiom} attribute.
172
+
173
+
/verificationLogger:<configuration>
174
+
Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format "trx;LogFileName=<...>");
175
+
176
+
The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option.
177
+
178
+
The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the isolate-assertions option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.
Copy file name to clipboardExpand all lines: latest/DafnyRef/README.md
+7-8Lines changed: 7 additions & 8 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -30,7 +30,7 @@ subfolders. In order to render files locally you must
30
30
* set the working directly (`cd`) to the `docs` folder (Windows or Ruby 3.0 users, see below for some tweaks)
31
31
* run the jekyll server: `bundle exec jekyll server`
32
32
* open a browser on the page http://localhost:4000 or directly to http://localhost:4000/DafnyRef/DafnyRef
33
-
* the server rerenders when files are changed -- but not always quite completely. Sometimes one must kill the server process, delete all the files in the _saite folder, and restart the server.
33
+
* the server rerenders when files are changed -- but not always quite completely. Sometimes one must kill the server process, delete all the files in the _site folder, and restart the server.
34
34
35
35
In order to convert markdown to pdf, you must be able to execute the Makefile, which requires installing pandoc and LaTeX, and being on a Linux-like platform.
36
36
@@ -64,12 +64,11 @@ definition file.
64
64
## On-line RM through github
65
65
Github uses rouge, via Jekyll. The syntax definition is a ruby-based file
66
66
maintained in the rouge github repo.
67
-
To modify the definition, follow the directions in
0 commit comments