diff options
Diffstat (limited to 'src/parser/options')
| -rw-r--r-- | src/parser/options | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/parser/options b/src/parser/options index f277b231d..c80914596 100644 --- a/src/parser/options +++ b/src/parser/options @@ -14,8 +14,18 @@ option memoryMap --mmap bool option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking disable ALL semantic checks, including type checks -# this is just to support security in the online version +# 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) -undocumented-option canIncludeFile /--no-include-file bool :default true +# 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 CVC4 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. +undocumented-option filesystemAccess /--no-filesystem-access bool :default true +undocumented-alias --no-include-file = --no-filesystem-access endmodule |