cprover
|
Value Set Abstract Object. More...
#include <analyses/variable-sensitivity/constant_abstract_value.h>
#include <analyses/variable-sensitivity/constant_pointer_abstract_object.h>
#include <analyses/variable-sensitivity/context_abstract_object.h>
#include <analyses/variable-sensitivity/interval_abstract_value.h>
#include <analyses/variable-sensitivity/two_value_array_abstract_object.h>
#include <analyses/variable-sensitivity/value_set_abstract_object.h>
Go to the source code of this file.
Classes | |
class | value_set_index_ranget |
Functions | |
index_range_ptrt | make_value_set_index_range (const abstract_object_sett &vals) |
exprt | rewrite_expression (const exprt &expr, const std::vector< abstract_object_pointert > &ops) |
std::vector< abstract_object_sett > | unwrap_operands (const std::vector< abstract_object_pointert > &operands) |
abstract_object_sett | unwrap_and_extract_values (const abstract_object_sett &values) |
abstract_object_pointert | maybe_extract_single_value (const abstract_object_pointert &maybe_singleton) |
Helper for converting singleton value sets into its only value. More... | |
abstract_object_pointert | maybe_unwrap_context (const abstract_object_pointert &maybe_wrapped) |
Helper for converting context objects into its abstract-value children maybe_wrapped: either an abstract value (or a set of those) or one wrapped in a context. More... | |
template<typename Con , typename F > | |
void | apply_comb (const std::vector< Con > &super_con, std::vector< typename Con::value_type > &sub_con, F f) |
Recursively construct a combination sub_con from super_con and once constructed call f . More... | |
template<typename Con , typename F > | |
void | for_each_comb (const std::vector< Con > &super_con, F f) |
Call the function f on every combination of elements in super_con . More... | |
Value Set Abstract Object.
Definition in file value_set_abstract_object.cpp.
void apply_comb | ( | const std::vector< Con > & | super_con, |
std::vector< typename Con::value_type > & | sub_con, | ||
F | f | ||
) |
Recursively construct a combination sub_con
from super_con
and once constructed call f
.
super_con | vector of some containers storing the values |
sub_con | the one combination being currently constructed |
f | callable with side-effects |
Definition at line 82 of file value_set_abstract_object.cpp.
void for_each_comb | ( | const std::vector< Con > & | super_con, |
F | f | ||
) |
Call the function f
on every combination of elements in super_con
.
Hence the arity of f
is super_con.size()
. <{1,2},{1},{1,2,3}> -> f(1,1,1), f(1,1,2), f(1,1,3), f(2,1,1), f(2,1,2), f(2,1,3).
super_con | vector of some containers storing the values |
f | callable with side-effects |
Definition at line 107 of file value_set_abstract_object.cpp.
index_range_ptrt make_value_set_index_range | ( | const abstract_object_sett & | vals | ) |
Definition at line 48 of file value_set_abstract_object.cpp.
abstract_object_pointert maybe_extract_single_value | ( | const abstract_object_pointert & | maybe_singleton | ) |
Helper for converting singleton value sets into its only value.
maybe_singleton:
either a set of abstract values or a single value
Definition at line 362 of file value_set_abstract_object.cpp.
abstract_object_pointert maybe_unwrap_context | ( | const abstract_object_pointert & | maybe_wrapped | ) |
Helper for converting context objects into its abstract-value children maybe_wrapped:
either an abstract value (or a set of those) or one wrapped in a context.
Definition at line 379 of file value_set_abstract_object.cpp.
exprt rewrite_expression | ( | const exprt & | expr, |
const std::vector< abstract_object_pointert > & | ops | ||
) |
Definition at line 321 of file value_set_abstract_object.cpp.
abstract_object_sett unwrap_and_extract_values | ( | const abstract_object_sett & | values | ) |
Definition at line 349 of file value_set_abstract_object.cpp.
std::vector< abstract_object_sett > unwrap_operands | ( | const std::vector< abstract_object_pointert > & | operands | ) |
Definition at line 333 of file value_set_abstract_object.cpp.