CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
variable-sensitivity Directory Reference
+ Directory dependency graph for variable-sensitivity:

Files

 abstract_aggregate_object.h
 Common behaviour for abstract objects modelling aggregate values - arrays, structs, etc.
 
 abstract_environment.cpp
 
 abstract_environment.h
 An abstract version of a program environment.
 
 abstract_object.cpp
 
 abstract_object.h
 abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual variables in the general non-relational domain.
 
 abstract_object_set.cpp
 
 abstract_object_set.h
 an unordered set of value objects
 
 abstract_object_statistics.h
 Statistics gathering for the variable senstivity domain.
 
 abstract_pointer_object.cpp
 
 abstract_pointer_object.h
 The base of all pointer abstractions.
 
 abstract_value_object.cpp
 
 abstract_value_object.h
 Common behaviour for abstract objects modelling values - constants, intervals, etc.
 
 constant_abstract_value.cpp
 
 constant_abstract_value.h
 An abstraction of a single value that just stores a constant.
 
 constant_pointer_abstract_object.cpp
 
 constant_pointer_abstract_object.h
 An abstraction of a pointer that tracks a single pointer.
 
 context_abstract_object.cpp
 
 context_abstract_object.h
 General implementation of a an abstract_objectt which can track side information in the form of a 'context' associated with a wrapped abstract_objectt of some other type.
 
 data_dependency_context.cpp
 Maintain data dependencies as a context in the variable sensitivity domain.
 
 data_dependency_context.h
 Maintain data dependencies as a context in the variable sensitivity domain.
 
 full_array_abstract_object.cpp
 
 full_array_abstract_object.h
 An abstraction of an array value.
 
 full_struct_abstract_object.cpp
 
 full_struct_abstract_object.h
 An abstraction of a structure that stores one abstract object per field.
 
 interval_abstract_value.cpp
 
 interval_abstract_value.h
 An interval to represent a set of possible values.
 
 liveness_context.cpp
 
 liveness_context.h
 Maintain a context in the variable sensitvity domain that records the liveness region for a given abstract_objectt.
 
 location_update_visitor.h
 
 map_visit.h
 
 three_way_merge_abstract_interpreter.cpp
 An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivity domain's three-way-merge operation on returning from a function call.
 
 three_way_merge_abstract_interpreter.h
 An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivity domain's three-way-merge operation on returning from a function call.
 
 two_value_array_abstract_object.h
 The base type of all abstract array representations.
 
 two_value_pointer_abstract_object.cpp
 
 two_value_pointer_abstract_object.h
 
 two_value_struct_abstract_object.h
 The base of all structure abstractions.
 
 two_value_union_abstract_object.h
 The base of all union abstractions.
 
 value_set_abstract_object.cpp
 Value Set Abstract Object.
 
 value_set_abstract_object.h
 Value Set Abstract Object.
 
 value_set_pointer_abstract_object.cpp
 Value Set of Pointer Abstract Object.
 
 value_set_pointer_abstract_object.h
 Value Set of Pointer Abstract Object.
 
 variable_sensitivity_configuration.cpp
 Captures the user-supplied configuration for VSD, determining which domain abstractions are used, flow sensitivity, etc.
 
 variable_sensitivity_configuration.h
 Captures the user-supplied configuration for VSD, determining which domain abstractions are used, flow sensitivity, etc.
 
 variable_sensitivity_dependence_graph.cpp
 
 variable_sensitivity_dependence_graph.h
 A forked and modified version of analyses/dependence_graph.
 
 variable_sensitivity_domain.cpp
 
 variable_sensitivity_domain.h
 There are different ways of handling arrays, structures, unions and pointers.
 
 variable_sensitivity_object_factory.cpp
 
 variable_sensitivity_object_factory.h
 Tracks the user-supplied configuration for VSD and build the correct type of abstract object when needed.
 
 widened_range.cpp
 
 widened_range.h
 
 write_location_context.cpp
 
 write_location_context.h
 Maintain a context in the variable sensitvity domain that records write locations for a given abstract_objectt.
 
 write_stack.cpp
 Represents a stack of write operations to an addressable memory location.
 
 write_stack.h
 Represents a stack of write operations to an addressable memory location.
 
 write_stack_entry.cpp
 Represents an entry in the write_stackt.
 
 write_stack_entry.h
 Represents an entry in the write_stackt.