cprover
Loading...
Searching...
No Matches
analyses Directory Reference
Directory dependency graph for analyses:

Directories

 
variable-sensitivity

Files

 
ai.cpp
 Abstract Interpretation.
 
ai.h
 Abstract Interpretation.
 
ai_domain.cpp
 Abstract Interpretation Domain.
 
ai_domain.h
 Abstract Interpretation Domain.
 
ai_history.cpp
 Abstract Interpretation history.
 
ai_history.h
 Abstract Interpretation history.
 
ai_storage.h
 Abstract Interpretation Storage.
 
call_graph.cpp
 Function Call Graphs.
 
call_graph.h
 Function Call Graphs.
 
call_graph_helpers.cpp
 Function Call Graph Helpers.
 
call_graph_helpers.h
 Function Call Graph Helpers.
 
call_stack_history.cpp
 History for tracking the call stack and performing interprocedural analysis.
 
call_stack_history.h
 History for tracking the call stack and performing interprocedural analysis.
 
cfg_dominators.h
 Compute dominators for CFG of goto_function.
 
constant_propagator.cpp
 Constant Propagation.
 
constant_propagator.h
 Constant propagation.
 
custom_bitvector_analysis.cpp
 Field-insensitive, location-sensitive bitvector analysis.
 
custom_bitvector_analysis.h
 Field-insensitive, location-sensitive bitvector analysis.
 
dependence_graph.cpp
 Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
 
dependence_graph.h
 Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
 
dirty.cpp
 Local variables whose address is taken.
 
dirty.h
 Variables whose address is taken.
 
does_remove_const.cpp
 Analyses.
 
does_remove_const.h
 Analyses.
 
escape_analysis.cpp
 Field-insensitive, location-sensitive escape analysis.
 
escape_analysis.h
 Field-insensitive, location-sensitive, over-approximative escape analysis.
 
flow_insensitive_analysis.cpp
 Flow Insensitive Static Analysis.
 
flow_insensitive_analysis.h
 Flow Insensitive Static Analysis.
 
global_may_alias.cpp
 Field-insensitive, location-sensitive global may alias analysis.
 
global_may_alias.h
 Field-insensitive, location-sensitive, over-approximative escape analysis.
 
goto_rw.cpp
 
goto_rw.h
 
guard.h
 Guard Data Structure.
 
guard_bdd.cpp
 Implementation of guards using BDDs.
 
guard_bdd.h
 Guard Data Structure Implementation using BDDs.
 
guard_expr.cpp
 Symbolic Execution.
 
guard_expr.h
 Guard Data Structure.
 
interval_analysis.cpp
 Interval Analysis – implements the functionality necessary for performing abstract interpretation over interval domain for goto programs.
 
interval_analysis.h
 Interval Analysis.
 
interval_domain.cpp
 Interval Domain.
 
interval_domain.h
 Interval Domain.
 
invariant_propagation.cpp
 Invariant Propagation.
 
invariant_propagation.h
 Invariant Propagation.
 
invariant_set.cpp
 Invariant Set.
 
invariant_set.h
 Value Set.
 
invariant_set_domain.cpp
 Invariant Set Domain.
 
invariant_set_domain.h
 Value Set.
 
is_threaded.cpp
 Over-approximate Concurrency for Threaded Goto Programs.
 
is_threaded.h
 Over-approximate Concurrency for Threaded Goto Programs.
 
lexical_loops.h
 Compute lexical loops in a goto_function.
 
local_bitvector_analysis.cpp
 Field-insensitive, location-sensitive may-alias analysis.
 
local_bitvector_analysis.h
 Field-insensitive, location-sensitive bitvector analysis.
 
local_cfg.cpp
 CFG for One Function.
 
local_cfg.h
 CFG for One Function.
 
local_control_flow_history.cpp
 Track function-local control flow for loop unwinding and path senstivity.
 
local_control_flow_history.h
 Track function-local control flow for loop unwinding and path senstivity.
 
local_may_alias.cpp
 Field-insensitive, location-sensitive may-alias analysis.
 
local_may_alias.h
 Field-insensitive, location-sensitive may-alias analysis.
 
local_safe_pointers.cpp
 Local safe pointer analysis.
 
local_safe_pointers.h
 Local safe pointer analysis.
 
locals.cpp
 Local variables.
 
locals.h
 Local variables whose address is taken.
 
loop_analysis.h
 Data structure representing a loop in a GOTO program and an interface shared by all analyses that find program loops.
 
natural_loops.h
 Compute natural loops in a goto_function.
 
reaching_definitions.cpp
 Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
 
reaching_definitions.h
 Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
 
sese_regions.cpp
 Single-entry, single-exit region analysis.
 
sese_regions.h
 Single-entry, single-exit region analysis.
 
uncaught_exceptions_analysis.cpp
 Over-approximating uncaught exceptions analysis.
 
uncaught_exceptions_analysis.h
 Over-approximative uncaught exceptions analysis.
 
uninitialized_domain.cpp
 Detection for Uninitialized Local Variables.
 
uninitialized_domain.h
 Detection for Uninitialized Local Variables.