StaticSemanticAnalysis

Classic semantic analysis involving pointers, data-flow, numerical values. This analysis always analyses the whole program

Required inputs: IR

Some checks require a more involved analysis of the possible runtime effects and values. These properties are undecidable in nature and the attempt to approximate them typically requires a lot more runtime and memory than other checks and often produces some false positives.

Possible Messages

This rule has no predefined messages.

Options

The following places define options that affect this rule: Analysis-GlobalOptions

debugging

Options that can help to debug the analysis.
 

debugging.dump_as_dot : bool = False

Description
Selects whether the constraint graph is dumped as text or into a dot file when option dump_final_constraint_graph or dump_initial_constraint_graph is used.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:no impact
Performance:less

 

debugging.dump_final_constraint_graph : bool = False

Description
Print the final constraint graph.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:no impact
Performance:less

 

debugging.dump_initial_constraint_graph : bool = False

Description
Print the constraint graph before solving starts.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:no impact
Performance:less

 

debugging.logging_level

Type: AxivionLoggingLevel

Default: 'ERROR'

Description
Set this to see more verbose output during analysis execution.

Technical notes
Setting this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:no impact
Performance:less if different from None

 

performance

Options that impact the runtime, memory, and precision of the analysis engine but do not hide possible findings.
 

performance.advanced

Performance and precision options that are only useful for specific language or project features
 

performance.advanced.additional_array_equalities : bool = True

Description
Let abstract-interpretation-based analysis compute additional array equality constraints. These constraints allow the symbolic expression domain to infer facts of the form i==j ==> a[i] == a[j]. This makes the analysis more precise, but can be slow if many array operations are present.

Relation to other options
An abstract-interpretation-based analysis has to be enabled for this option to have an effect. See the option performance.general.enhanced_analysis for details on how to enable such an analysis.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.advanced.buffer_analysis_precision_threshold : int = 1500

Description
For some rules, the abstract-interpretation-based analysis tries to infer which arrays are buffers (i.e., are null-terminated, or segmented into multiple null-terminated parts). For this, is computes various constraints for each source code location. If more constraints than this threshold are computed, the abstract-interpretation-based analysis switches to a coarse overapproximation for this routine.
Set to 0 to disable the threshold.

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:more (0 most)
Performance:less (0 slowest)

 

performance.advanced.enum_analysis_precision_threshold : int = 50000

Description
For some rules, the abstract-interpretation-based analysis tries to infer if a variable value is a valid enumerator for one or more of the available enum types. If there are more variable-value pairs than this threshold at a source code location, abstract-interpretation-based analysis disables this inference for the current routine.
Set to 0 to disable the threshold.

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:more (0 most)
Performance:less (0 slowest)

 

performance.advanced.null_analysis_enhanced_precision : bool = True

Description
Whether analysis of null dereferences should track more facts about symbolic (i.e. indirectly accessed) memory locations like a->b across routine borders.
For example, for a struct S having a field f of pointer type, the enhanced precision can help avoiding false positives in situations similar to the following example. 

void do_it(S* param)
{
    // information ps->f != nullptr transferred from (single) caller
    // to parameter param
    *(param->f) = ...
}

int main(void)
{
    S* ps;
    ...
    if (ps->f != nullptr)
    {
        do_it(ps);
    }
    return 0;
}

Relation to other options
Either the option performance.general.enhanced_analysis or the option performance.pointer_analysis.use_abstract_interpretation_for_null has to be enabled for this option to have an effect.
The following rules check for null pointer dereferences and are affected by this option.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.advanced.references_analysis

Options for specialized analyses tracking validity properties of pointers and references.
 

performance.advanced.references_analysis.abstract_references_analysis : bool = True

Description
Use additional abstract references analysis to refine results of the null pointer check. The analysis tracks facts for smartpointers and iterators (referred to as "abstract reference" types). The analysis uses specifications given via Externals rules to interpret the effect of operators like operator== etc. for abstract references. For own iterator / smartpointer types, additional Externals rules can be specified. The types of abstract references that have to be tracked are specified in the rule Externals-AbstractReferenceTypes.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact (assuming external specifications are correct)
Precision:more
Performance:less

 

performance.advanced.references_analysis.abstract_references_precision_threshold : int = 200

Description
If additional abstract references analysis is active: controls precision of tracked facts about abstract references. Higher value means more precision.

Technical notes
Increasing this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.advanced.symbolic_expressions_precision_threshold : int = 1500

Description
If more symbolic expression facts are computed than this threshold at a source code location, the symbolic analysis switches into a very coarse mode for the routine.
Set to 0 to disable the threshold.

Relation to other options
An abstract-interpretation-based analysis has to be enabled for this option to have an effect. See the option performance.general.enhanced_analysis for details on how to enable such an analysis.

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:more (0 most)
Performance:less (0 slowest)

 

performance.advanced.use_full_pointer_analysis : bool = False

Description
Run the more precise but also more costly full pointer analysis even if no rule requests it.

Relation to other options
Most semantic analysis rules force the execution of a full pointer analysis and this option has no effect. The rules concerned with exception behavior (FaultDetection-*except*) do not require a full pointer analysis, but can benefit from it. For specific configurations, where one is only interested in these exception rules, one can enable this option to run the more precise but also more costly full pointer analysis.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general

Performance and precision options that are useful for most situations.
 

performance.general.abstract_interpretation_coarse_callcycle_analysis : bool = False

Description
Let abstract-interpretation-based analysis compute a fixpoint for recursive function calls instead of using an overapproximation.

Relation to other options
An abstract-interpretation-based analysis has to be enabled for this option to have an effect. See the option performance.general.enhanced_analysis for details on how to enable such an analysis.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:less
Performance:more

 

performance.general.abstract_value_analysis_options

Options controlling the precision of the abstract value analysis. These options are only relevant if performance.general.abstract_value_analysis_options.abstract_value_analysis is set to true.
 

performance.general.abstract_value_analysis_options.abstract_value_analysis : bool = True

Description
Use an additional intra-procedural analysis after the initial value propagation. This analysis tracks numerical information of symbolic memory locations like a->b or a[i]. It can, for example, infer that x > 42 holds in if (a->b > 42) { int x = a->b; }.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.abstract_value_analysis_options.analyse_system_includes : bool = False

Description
Controls whether the abstract value analysis also should analyse files in system includes. Should only be set to true if findings for system includes are also configured to be reported.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.abstract_value_analysis_options.interval_precision_threshold : int = 250

Description
If more numerical facts for memory locations are computed than this threshold at a source code location, the analysis switches into a very coarse mode for the routine. This can help speeding up the analysis in the case of large routines.
Set to 0 to disable the threshold.

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.abstract_value_analysis_options.maximal_cfg_size : int = 1000

Description
Abstract value analysis is only executed for functions having less or equal control flow blocks than the value of this option. It can be used to exclude excessively large and complex routines from the abstract value analysis.
Set to 0 to disable the threshold.

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.abstract_value_analysis_options.perform_initial_pass : bool = False

Description
Perform a light-weight variant of abstract value analysis before the initial value propagation. This pass propagates information about inequalities of symbolic memory locations to the initial value propagation.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.abstract_value_analysis_options.widening_threshold : int = 5

Description
Controls how soon the abstract value analysis tries to overapproximate effects of loops. A higher value of this option can improve the precision of computed numerical information, but can also make the analysis slower.

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.array_analysis_options

Configuration options for array analyses.
 

performance.general.array_analysis_options.array_analysis : bool = True

Description
Use additional array analysis to compute possible values for arrays containing numerical values or pointer values. Further analyses can then assume that a read of an array element is one of the values computed by the analysis. E.g., 

int arr[4] = {1,2,3,4};
... // no write for arr
arr[3] = 10;
...  // no write for arr
int x = arr[i]; // x in range [1, 10]
Soundness is affected in the case of out-of-bounds accesses: the analysis is allowed to assume the pre-computed values for each array element access, even if it is possibly out-of-bounds (e.g. if i = 4 in the example).

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness (see description)
Precision:more
Performance:less

 

performance.general.array_analysis_options.numerical_precision : int = 20

Description
If additional array analysis is active: controls precision of tracked numerical information for arrays. Higher value means more precision.

Technical notes
Increasing this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.array_analysis_options.pointer_precision : int = 20

Description
If additional array analysis is active: controls precision of tracked pointer information for arrays. Higher value means more precision.

Technical notes
Increasing this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.enhanced_analysis : bool = False

Description
Run additional abstract-interpretation-based analysis in different rules.

Relation to other options
Instead of enabling this option, you can also selectively enable it for certain rules. If this option is enabled, it takes precedence over the selective options. The following rules check for division-by-zero, overflow, and out-of-bounds. Each of them has an option to selectively enable an additional abstract-interpretation-based analysis.


For the following rules, an additional abstract-interpretation-based analysis can be enabled with the option performance.pointer_analysis.use_abstract_interpretation_for_null.

Technical notes
This analysis uses symbolic expressions and special domains for tracking null dereferences.
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.field_mod_analysis_options

Configuration options for initial field-mod analysis.
 

performance.general.field_mod_analysis_options.field_mod_analysis : bool = True

Description
Use additional analysis to infer properties that hold globally for the values stored in specific fields. Soundness is affected if there are instances where fields are not initialized: the analysis might exclude cases involving uninitialized (arbitrary) values. To identify such cases when the analysis is active, it is advisable to enable rules that detect uninitialized accesses, like FaultDetection-UninitializedVariable.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.
Soundness:prevents soundness (see description)
Precision:more
Performance:less

 

performance.general.loop_counter_relations_analysis : bool = True

Description
Whether an additional intra-procedural analysis for relations between loop counters and other routine-local variables values should be carried out.
This analysis can help avoiding false positives by, e.g., inferring that x <= 2*i holds after the loop in the following code snippet. 

int array[30];
int x = 0;
for(int i = 0; i < 10; ++i)
{
    if (cond) { x++; }
    else { x += 2; }
}
array[x] = ...
For checking whether the array access arr[x] is out-of-bounds, the analysis can use the inferred info that x is not larger than 20.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.query_timeout : int = 5000

Description
Time limit in milliseconds for single SMT queries during abstract-interpretation-based analysis.
Set to 0 to disable the time limit completely (which may prevent the analysis from terminating).

Relation to other options
An abstract-interpretation-based analysis has to be enabled for this option to have an effect. See the option performance.general.enhanced_analysis for details on how to enable such an analysis.

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:more (0 most)
Performance:less (0 slowest, might run forever)

 

performance.general.routine_context_granularity : int = 4

Description
The number of calling contexts to distinguish (between 1 and 8). A higher number of contexts allows a more precise analysis but typically also requires longer runtime and higher memory consumption. A context considers a routine when called from a certain caller, excluding the effects of other callers.

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.transfer_additional_results : bool = False

Description
Refine base analysis results directly with abstract-interpretation-based analysis.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.general.union_find_points_to_analysis : bool = False

Description
If true, union-find-based points-to analysis will run. Its results might speed up subsequent analyses by excluding cases of aliasing. Its results are also used to refine the call graph if semantics.advanced.use_coarse_callgraph is set to True.

Technical notes
Activating this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:can increase precision
Performance:Can speed up subsequent analyses, but requires initial analysis time

 

performance.pointer_analysis

Performance and precision options related to handling of pointers and references.
 

performance.pointer_analysis.cache_reset_threshold : int = 25000000

Description
Threshold after which the internal BDD-based cache for points-to sets during pointer analysis is cleared (set to 0 to never clear it).

Technical notes
Higher values of this option affect soundness, precision, and performance as follows.

Soundness:no impact
Precision:no impact
Performance:faster, requires more memory

 

performance.pointer_analysis.conservative_method_pointer_calls : bool = False

Description
Precompute method pointer call targets using a conservative approximation. This can speed up analyses, but might result in less precise analysis results.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:less
Performance:more

 

performance.pointer_analysis.process_subobject_casts : bool = True

Description
Refine pointer target types for subobjects during dynamic casts.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

performance.pointer_analysis.use_abstract_interpretation_for_null : bool = False

Description
Refine pointer analysis results with results from abstract-interpretation-based analysis to improve null pointer target propagation.

Relation to other options
This option has no effect when performance.general.enhanced_analysis is enabled.
The following rules check for null pointer dereferences and are affected by this option.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:less

 

semantics

Options that not only impact the runtime, memory, and precision of the analysis engine, but may also hide potential findings.
 

semantics.advanced

Options that affect analysis semantics and are only useful for specific language or project features
 

semantics.advanced.address_taken_functions_as_entries

Type: AddressTakenEntryPoints

Default: 'IGNORE'

Description
Controls whether the analysis should treat functions as additional entry points if their address is taken and possibly passed to an external function. This is for example useful to handle pthread_create(..., &func, ...).

For a more fine-tuned approach to these cases, consider using EntryPoints to manually configure entry points.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for analyzing functions being only called from external code to which their address is passed
Precision:adds more findings
Performance:less

 

semantics.advanced.allow_function_pointer_signature_mismatch : bool = False

Description
Allow usage of function pointer targets with mismatching signatures in indirect calls.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for soundness
Precision:depends
Performance:less

 

semantics.advanced.apply_base_cast_fix : bool = False

Description
Adapt base-class pointer type for certain casts on structured memory created by functions with custom placement new parameters or certain std implementations (e.g., MSVC std::function).

Relation to other options
The option semantics.pointer_analysis.use_pointer_filter has to be enabled for this option to have an effect.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for soundness
Precision:less or same
Performance:may significantly increase analysis cost in time and space

 

semantics.advanced.apply_base_cast_split_fix : bool = False

Description
Activate fix to properly handle base-class pointer casts combined with two indirections. This option is required for proper analysis of many shared_ptr implementations.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for soundness
Precision:less or same
Performance:may significantly increase analysis cost in time and space

 

semantics.advanced.apply_placement_new_fix : bool = False

Description
Handle objects created with placement new correctly.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for soundness
Precision:less
Performance:slower

 

semantics.advanced.apply_virtual_call_this_adjustment : bool = False

Description
Apply dynamic cast to the derived class type during virtual calls s.t. the type of this inside the called method is the actual type and not the base type.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for soundness
Precision:more
Performance:no impact

 

semantics.advanced.assume_reference_address_nonnull : bool = True

Description
Assume that addresses of C++ references are always non-null.

Since it is undefined behavior to initialize a reference with the dereference of a pointer that is potentially nullptr, assume that the address of a reference is never nullptr. Disabling this option may lead to more findings where the analysis cannot confirm the non-nullness.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Suppresses false positives where the analysis cannot be sure about the non-nullnessImproved performance due to less false-positive data-flow propagations
Soundness:Suppresses valid findings for constructs like auto &r = *p where p may or must be nullptr
Precision:depends
Performance:depends

 

semantics.advanced.char_is_like_void : bool = False

Description
Treat char* objects like void* when filtering for compatible types during pointer analysis, i.e., char* then is universally compatible.

Relation to other options
The option semantics.pointer_analysis.use_pointer_filter has to be enabled for this option to have an effect.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for soundness
Precision:depends on project
Performance:less

 

semantics.advanced.compare_parameter_types : bool = False

Description
Allow indirect calls in callgraph only if parameter types match.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness
Precision:depends
Performance:more

 

semantics.advanced.filter_enums_to_enumerator_range : bool = True

Description
Assume that values of enum type are within the bounds of their enumerators. This assumption is, e.g., not true if enums are used for implementing flags.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness if the analysed code violates the assumption
Precision:more
Performance:faster

 

semantics.advanced.ignore_strings : bool = False

Description
Exclude string literals from propagation as pointer targets.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness
Precision:more
Performance:more

 

semantics.advanced.treat_uncalled_functions_as_alive : bool = False

Description
Assume that all uncalled functions are additional entry points.

Note that in most circumstances, not all uncalled functions are entry points. Enabling this option will then lead to false positives and longer analysis times. Hence, before using this option, consider using EntryPoints or manual drivers.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness if the analysed code violates the assumption
Precision:depends
Performance:depends

 

semantics.advanced.use_coarse_callgraph : bool = False

Description
Overapproximate function pointer targets during callgraph generation.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness
Precision:less
Performance:more

 

semantics.advanced.use_symbolic_external_objects : bool = False

Description
Create symbolic objects for unspecified external functions returning pointer types and for entry points with pointer parameters.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness
Precision:less
Performance:less

 

semantics.enable_filtering_heuristics : bool = False

Description
Allow all analyses to use heuristics to exclude findings which are probably false positives.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness
Precision:more
Performance:more

 

semantics.exceptions

Options related to exceptions.
 

semantics.exceptions.base_class_for_throw_any : bauhaus.analysis.config.QualifiedName = ''

Description
Specifies the base class of exceptions for external functions that can throw exceptions. If this option is not set, these functions can throw any exception. Per-function exception behavior can also be specified with Externals-FunctionSummary.

Technical notes
Setting this option affects soundness, precision, and performance as follows.

Soundness:specifying the wrong base class is unsound
Precision:more
Performance:more

 

semantics.exceptions.ignore_exceptions : bool = False

Description
Assume that no exception is thrown and do not track exceptions.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness
Precision:more
Performance:more

 

semantics.exceptions.missing_specifier_means_throw_any : bool = False

Description
Treat external functions with neither throw(...), nor noexcept(...), nor an explicit exception configuration under configuration group Externals as if they were declared with noexcept(true).
Disabling this options treats them as if they were declared with noexcept(false).
Disabling this option leads to faster analysis, but might be unsound (depending on the language level).

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:depends
Precision:more
Performance:less

 

semantics.pointer_analysis

Options related to handling of pointers and references.
 

semantics.pointer_analysis.apply_compound_cast_fix : bool = False

Description
Propagate pointer targets between fields during assignment of structured objects.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for soundness
Precision:less
Performance:slower

 

semantics.pointer_analysis.assume_pointer_parameters_of_entries_nonnull : bool = False

Description
Assume that pointer-typed parameters of entry functions are not null.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness if the analysed code violates the assumption
Precision:depends
Performance:no impact

 

semantics.pointer_analysis.restrict_all_integers_storing_pointers : bool = False

Description
Assume that no integer variable can store a pointer.

Relation to other options
The option semantics.pointer_analysis.use_pointer_filter has to be enabled for this option to have an effect.

If this option is enabled, the option semantics.pointer_analysis.restrict_bit_size_for_integers_storing_pointers has no effect.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness if the analysed code violates the assumption
Precision:more
Performance:more

 

semantics.pointer_analysis.restrict_bit_size_for_integers_storing_pointers : bool = True

Description
Assume that an integer variable which stores a pointer has to have at least the bit size of (void*). This assumption might be violated for systems where pointers have different sizes, e.g. in connection with near and far pointers in older DOS systems.

Relation to other options
The option semantics.pointer_analysis.use_pointer_filter has to be enabled for this option to have an effect.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness if the analysed code violates the assumption
Precision:more
Performance:more

 

semantics.pointer_analysis.summarize_simple_calls : bool = True

Description
Attempt to improve the precision for calls where the return value computation in the called function is simple enough and returns one of the parameters or a subobject of such a parameter.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:no impact
Precision:more
Performance:more

 

semantics.pointer_analysis.untyped_heap_handling : bool = False

Description
Update pointer targets of structured object fields when assigning untyped heap objects to structured objects. Disabling this option makes the pointer analysis for these situations unsound.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:required for soundness
Precision:less
Performance:less

 

semantics.pointer_analysis.use_integer_zero_as_null : bool = False

Description
If true, integer zero is propagated similar to a nullptr value in pointer analysis. This can lead to more findings in checks for null-pointer dereferences.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:more
Precision:less
Performance:less

 

semantics.pointer_analysis.use_pointer_filter : bool = False

Description
Assume that objects of character, floating point or bool type cannot represent pointer targets.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness if the analysed code violates the assumption
Precision:less
Performance:more

 

semantics.pointer_analysis.use_type_filter : bool = False

Description
Use type-based heuristics to filter out potential false positives in the pointer analysis and in all use-after-free checks. This option might introduce false negatives (i.e., missing pointer targets) e.g. in the context of explicit casts between pointers to integral types of different sizes.

Technical notes
Enabling this option affects soundness, precision, and performance as follows.

Soundness:prevents soundness
Precision:more
Performance:more

 

Option Types

These types are used by options listed above:

AddressTakenEntryPoints

Enumerates the different options for dealing with address-taken functions
 

  • IGNORE

  • ALL

  • EXTERNALS

AxivionLoggingLevel

An enumeration.
 

  • NONE

  • DEBUG

  • INFO

  • WARNING

  • ERROR

  • CRITICAL