#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#

module PARSER "options/parser_options.h" Parser

common-option strictParsing --strict-parsing bool
 be less tolerant of non-conforming inputs

option memoryMap --mmap bool
 memory map file input

option semanticChecks semantic-checks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
 disable ALL semantic checks, including type checks

option globalDeclarations global-declarations bool :default false
 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 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 filesystem-access /--no-filesystem-access bool :default true
undocumented-alias --no-include-file = --no-filesystem-access

endmodule