Fields - continue_on_unknown_instruction :: Bool
When encountering an unknown instruction do we either
* report it to stderr but continue (True), or
* exit with an error message (False)?
Sane default: True - generate_pdfs :: Bool
Do we call graphviz to generate PDFs?
Set to true for small examples, false for larger ones. - verbose_logs :: Bool
Must the invariants be stored in the logs?
Sane default: False - store_preconditions_in_L0 :: Bool
Must preconditions be stored in the .L0 file?
Set to true for small examples, false for larger ones.
Sane default: False - store_assertions_in_L0 :: Bool
Must assertions be stored in the .L0 file?
Set to true for small examples, false for larger ones.
Sane default: False - max_time :: Natural
The maximum verification time in seconds per function
Sane default: 30 minutes = 000000 * 60 * 30 = 1800000000 - max_num_of_cases :: Natural
The maximum number of separate concrete cases considered non-deterministically, before abstraction is applied.
Has no effect on soundness, but lower values cause more abstraction.
Sane default: 5 - max_num_of_bases :: Natural
The maximum number of pointer bases a bottom-expression may have, before more asbtraction is applied.
Has no effect on soundness, but lower values cause more abstraction.
Sane default: 25 - max_num_of_sources :: Natural
- max_jump_table_size :: Natural
The maximum number of sources a bottom-expression may have, before resorting to rock-bottom.
Has no effect on soundness, but lower values cause more abstraction.
Sane default: 100 - max_expr_size :: Natural
The maximum size of an expression (counting each operator and each leaf as 1), before a symbolic expression is abstracted to rock bottom.
Does not affect soundness, but if the value is set too low, then the results becomes overly overapproximative.
Sane default: 3000 - nasm_with_safe_labels :: Bool
If set to True, then the NASM code will have longer labels (less readable) but always correct.
If set to False, labels may occur twice preventing compilation.
Sane default: True
|