CBMC
|
#include "variable_sensitivity_object_factory.h"
#include "constant_abstract_value.h"
#include "constant_pointer_abstract_object.h"
#include "data_dependency_context.h"
#include "full_array_abstract_object.h"
#include "full_struct_abstract_object.h"
#include "interval_abstract_value.h"
#include "liveness_context.h"
#include "two_value_array_abstract_object.h"
#include "two_value_pointer_abstract_object.h"
#include "two_value_struct_abstract_object.h"
#include "two_value_union_abstract_object.h"
#include "value_set_abstract_object.h"
#include "value_set_pointer_abstract_object.h"
Go to the source code of this file.
Functions | |
template<class context_classt > | |
abstract_object_pointert | create_context_abstract_object (const abstract_object_pointert &abstract_object) |
template<class abstract_object_classt > | |
abstract_object_pointert | create_abstract_object (const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns) |
abstract_object_pointert | wrap_with_context_object (const abstract_object_pointert &abstract_object, const vsd_configt &configuration) |
template<class abstract_object_classt > | |
abstract_object_pointert | initialize_abstract_object (const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns, const vsd_configt &configuration) |
Function: variable_sensitivity_object_factoryt::initialize_abstract_object Initialize the abstract object class and return it. More... | |
abstract_object_pointert create_abstract_object | ( | const typet | type, |
bool | top, | ||
bool | bottom, | ||
const exprt & | e, | ||
const abstract_environmentt & | environment, | ||
const namespacet & | ns | ||
) |
Definition at line 34 of file variable_sensitivity_object_factory.cpp.
abstract_object_pointert create_context_abstract_object | ( | const abstract_object_pointert & | abstract_object | ) |
Definition at line 27 of file variable_sensitivity_object_factory.cpp.
abstract_object_pointert initialize_abstract_object | ( | const typet | type, |
bool | top, | ||
bool | bottom, | ||
const exprt & | e, | ||
const abstract_environmentt & | environment, | ||
const namespacet & | ns, | ||
const vsd_configt & | configuration | ||
) |
Function: variable_sensitivity_object_factoryt::initialize_abstract_object Initialize the abstract object class and return it.
type | the type of the variable |
top | whether the abstract object should be top in the two-value domain |
bottom | whether the abstract object should be bottom in the two-value domain |
e | if top and bottom are false this expression is used as the starting pointer for the abstract object |
environment | the current abstract environment |
ns | namespace, used when following the input type |
configuration | variable sensitivity domain configuration |
Definition at line 84 of file variable_sensitivity_object_factory.cpp.
abstract_object_pointert wrap_with_context_object | ( | const abstract_object_pointert & | abstract_object, |
const vsd_configt & | configuration | ||
) |
Definition at line 49 of file variable_sensitivity_object_factory.cpp.