smithy-dafny/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml at a9d57f9215b8f60d57f307e2f6fc230589f823cf · smithy-lang/smithy-dafny · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
includes = [
  "../dafny/Source/DafnyStandardLibraries/src/Std/Actions/Actions.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Actions/Aggregators.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Actions/Enumerators.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Actions/GenericAction.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/BoundedInts.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/DynamicArray.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Frames.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Math.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Relations.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Streams/Streams.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Termination.dfy",
  "../dafny/Source/DafnyStandardLibraries/src/Std/Wrappers.dfy"
]

[options]
# Options that help support more values of consuming context options
# (mostly turning on any more restrictive verification)
track-print-effects = true
enforce-determinism = true
reads-clauses-on-methods = true

# Options that differ from Dafny's
unicode-char = false

# TODO
allow-warnings = true

# Options important for sustainable development
# of the libraries themselves.
resource-limit = 1000000
# These give too many false positives right now, but should be enabled in the future
warn-redundant-assumptions = false
warn-contradictory-assumptions = false