blob: 4b3d01b9972615d25a40a2b5f3335ab18df5d382 (
plain)
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
id = "PARSER"
name = "Parser"
[[option]]
name = "strictParsing"
category = "common"
long = "strict-parsing"
type = "bool"
help = "be less tolerant of non-conforming inputs"
[[option]]
name = "memoryMap"
category = "regular"
long = "mmap"
type = "bool"
help = "memory map file input"
[[option]]
name = "semanticChecks"
smt_name = "semantic-checks"
category = "regular"
type = "bool"
default = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
help = "enable semantic checks, including type checks"
[[option]]
name = "globalDeclarations"
smt_name = "global-declarations"
category = "regular"
type = "bool"
default = "false"
help = "force all declarations and definitions to be global"
# this is to support security in the online version, and in other similar
# contexts (--no-include-file disables filesystem access in TPTP and SMT2
# parsers) the name --no-include-file is legacy: it also now limits any
# filesystem access (read or write) for example by using --dump-to (or the
# equivalent set-option) or set-option
# :regular-output-channel/:diagnostic-output-channel. However, the main driver
# is still permitted to read the input file given on the command-line if any.
# creation/use of temp files are still permitted (but the paths aren't given by
# the user). Also note this is only safe for the version invoked through the
# main driver, there are ways via the API to get the cvc5 library to open a file
# for reading or writing and thus leak information from an existing file, or
# overwrite an existing file with malicious content.
[[option]]
name = "filesystemAccess"
category = "undocumented"
long = "filesystem-access"
type = "bool"
default = "true"
[[option]]
name = "forceLogicString"
smt_name = "force-logic"
category = "expert"
long = "force-logic=LOGIC"
type = "std::string"
help = "set the logic, and override all further user attempts to change it"
|
