Loading...

Searching...

No Matches

value_sett Class Reference

State type in value_set_domaint, used in value-set analysis and goto-symex. More...

#include <value_set.h>

+ Collaboration diagram for value_sett:

[フレーム]

[legend]

Classes

struct entryt

Represents a row of a value_sett . More...

Public Types

enum class insert_actiont { INSERT , RESET_OFFSET , NONE }

typedef std::optional< exprt > offsett

Represents the offset into an object: either some (possibly constant) expression, or an unknown value, represented by !offset.

using object_map_dt = std::map< object_numberingt::number_type, offsett >

Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).

using object_mapt = reference_counting< object_map_dt, empty_object_map >

Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances can share them.

typedef sharing_mapt< irep_idt, entryt > valuest

Map representing the entire value set, mapping from string LHS IDs to RHS expression sets.

Public Member Functions

value_sett ()

value_sett (value_sett &&other)

virtual ~value_sett ()=default

value_sett (const value_sett &other)=default

value_sett & operator= (const value_sett &other)=delete

value_sett & operator= (value_sett &&other)

virtual bool field_sensitive (const irep_idt &id, const typet &type)

Determines whether an identifier of a given type should have its fields distinguished.

exprt to_expr (const object_map_dt::value_type &it) const

Converts an object_map_dt element object_number -> offset into an object_descriptor_exprt with .object() == object_numbering.at(object_number) and .offset() == offset.

void set (object_mapt &dest, const object_map_dt::value_type &it) const

Sets an element in object map dest to match an existing element it from a different map.

bool insert (object_mapt &dest, const object_map_dt::value_type &it) const

Merges an existing element into an object map.

bool insert (object_mapt &dest, const exprt &src) const

Adds an expression to an object map, with unknown offset.

bool insert (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const

Adds a numbered expression and offset to an object map.

insert_actiont get_insert_action (const object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const

Determines what would happen if object number n was inserted into map dest with offset offset – the possibilities being, nothing (the entry is already present), a new entry would be inserted (no existing entry with number n was found), or an existing entry's offset would be reset (indicating there is already an entry with number n, but with differing offset).

bool insert (object_mapt &dest, const exprt &expr, const offsett &offset) const

Adds an expression and offset to an object map.

std::vector< exprt > get_value_set (exprt expr, const namespacet &ns) const

Gets values pointed to by expr, including following dereference operators (i.e.

void clear ()

const entryt * find_entry (const irep_idt &id) const

Finds an entry in this value-set.

void update_entry (const entryt &e, const typet &type, const object_mapt &new_values, bool add_to_sets)

Adds or replaces an entry in this value-set.

void output (std::ostream &out, const std::string &indent="") const

Pretty-print this value-set.

xmlt output_xml (void) const

Output the value set formatted as XML.

bool make_union (object_mapt &dest, const object_mapt &src) const

Merges two RHS expression sets.

bool make_union_would_change (const object_mapt &dest, const object_mapt &src) const

Determines whether merging two RHS expression sets would cause any change.

bool make_union (const valuest &new_values)

Merges an entire existing value_sett's data into this one.

bool make_union (const value_sett &new_values)

Merges an entire existing value_sett's data into this one.

void guard (const exprt &expr, const namespacet &ns)

Transforms this value-set by assuming an expression holds.

void apply_code (const codet &code, const namespacet &ns)

Transforms this value-set by executing a given statement against it.

void assign (const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)

Transforms this value-set by executing executing the assignment lhs := rhs against it.

void do_function_call (const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)

Transforms this value-set by executing the actual -> formal parameter assignments for a particular callee.

void do_end_function (const exprt &lhs, const namespacet &ns)

Transforms this value-set by assigning this function's return value to a given LHS expression.

void get_reference_set (const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const

Gets the set of expressions that expr may refer to, according to this value set.

bool eval_pointer_offset (exprt &expr, const namespacet &ns) const

Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-set's information.

std::optional< irep_idt > get_index_of_symbol (irep_idt identifier, const typet &type, const std::string &suffix, const namespacet &ns) const

Get the index of the symbol and suffix.

void erase_values_from_entry (const irep_idt &index, const std::unordered_set< exprt, irep_hash > &values_to_erase)

Update the entry stored at index by erasing any values listed in values_to_erase.

void erase_symbol (const symbol_exprt &symbol_expr, const namespacet &ns)

Public Attributes

unsigned location_number

Matches the location_number field of the instruction that corresponds to this value_sett instance in value_set_domaint's state map.

valuest values

Stores the LHS ID -> RHS expression set map.

Static Public Attributes

static object_numberingt object_numbering

Global shared object numbering, used to abbreviate expressions stored in value sets.

static const object_map_dt empty_object_map {}

Protected Member Functions

object_mapt get_value_set (exprt expr, const namespacet &ns, bool is_simplified) const

Reads the set of objects pointed to by expr, including making recursive lookups for dereference operations etc.

void get_reference_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const

See the other overload of get_reference_set.

void get_reference_set_rec (const exprt &expr, object_mapt &dest, const namespacet &ns) const

See get_reference_set.

void dereference_rec (const exprt &src, exprt &dest) const

Sets dest to src with any wrapping typecasts removed.

void erase_symbol_rec (const typet &type, const std::string &erase_prefix, const namespacet &ns)

void erase_struct_union_symbol (const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)

virtual void get_value_set_rec (const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns) const

Subclass customisation point for recursion over RHS expression.

virtual void assign_rec (const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)

Subclass customisation point for recursion over LHS expression:

virtual void apply_code_rec (const codet &code, const namespacet &ns)

Subclass customisation point for applying code to this domain:

Private Member Functions

virtual void adjust_assign_rhs_values (const exprt &rhs, const namespacet &, object_mapt &rhs_values) const

Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set before it is passed into assign.

virtual void apply_assign_side_effects (const exprt &lhs, const exprt &rhs, const namespacet &)

Subclass customisation point to apply global side-effects to this domain, after RHS values are read but before they are written.

Detailed Description

State type in value_set_domaint, used in value-set analysis and goto-symex.

Represents a mapping from expressions to the addresses that may be stored there; for example, a global that is either null or points to a heap-allocated object, which itself has two fields, one pointing to another heap object and the other having unknown target, would be represented:

global_x -> { null, <dynamic_object1, 0> }
dynamic_object1.field1 -> { <dynamic_object2, 0> }
dynamic_object1.field2 -> { * (unknown) }

LHS expressions can be either symbols or fields thereof, and are stored as strings; RHS expressions may be symbols, dynamic objects, integer addresses (as in (int*)0x1234) or unknown (printed as *), and are stored as pairs of an exprt and an optional offset if known (0 for both dynamic objects in the example given above). RHS expressions are represented using numbering to avoid storing redundant duplicate expressions.

Definition at line 42 of file value_set.h.

Member Typedef Documentation

◆ object_map_dt

using value_sett::object_map_dt = std::map<object_numberingt::number_type, offsett>

Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).

This is the RHS set of a single row of the enclosing value_sett , such as { null, dynamic_object1 }. The set is represented as a map from numbered exprts to offsett instead of a set of pairs to make lookup by exprt easier.

Definition at line 87 of file value_set.h.

◆ object_mapt

using value_sett::object_mapt = reference_counting<object_map_dt, empty_object_map>

Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances can share them.

For example, if we have a pair of instructions with value-sets:

x = new A;
 x -> { dynamic_object1 }
y = new B;
 x -> { dynamic_object1 }
 y -> { dynamic_object2 }

Then the set { dynamic_object1 }, represented by an object_map_dt, can be shared between the two value_sett instances.

Definition at line 109 of file value_set.h.

◆ offsett

typedef std::optional<exprt> value_sett::offsett

Represents the offset into an object: either some (possibly constant) expression, or an unknown value, represented by !offset.

Definition at line 80 of file value_set.h.

◆ valuest

typedef sharing_mapt<irep_idt, entryt> value_sett::valuest

Map representing the entire value set, mapping from string LHS IDs to RHS expression sets.

Note this data structure is somewhat denormalized, for example mapping

dynamic_object1.field2 ->
 entryt {
 .identifier = dynamic_object1,
 .suffix = .field2,
 .object_map = ...
 }

The components of the ID are thus duplicated in the valuest key and in entryt fields.

Definition at line 230 of file value_set.h.

Member Enumeration Documentation

◆ insert_actiont

enum class value_sett::insert_actiont

strong

Enumerator
INSERT
RESET_OFFSET
NONE

Definition at line 154 of file value_set.h.

Constructor & Destructor Documentation

◆ value_sett() [1/3]

value_sett::value_sett ( )

inline

Definition at line 45 of file value_set.h.

◆ value_sett() [2/3]

value_sett::value_sett ( value_sett && other )

inline

Definition at line 49 of file value_set.h.

◆ ~value_sett()

virtual value_sett::~value_sett ( )

virtualdefault

◆ value_sett() [3/3]

value_sett::value_sett ( const value_sett & other )

default

Member Function Documentation

◆ adjust_assign_rhs_values()

virtual void value_sett::adjust_assign_rhs_values ( const exprt & rhs,

const namespacet & ,

object_mapt & rhs_values

) const

inlineprivatevirtual

Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set before it is passed into assign.

For example, this is used in one subclass to tag and thus differentiate values that originated in a particular place, vs. those that have been copied.

Definition at line 499 of file value_set.h.

◆ apply_assign_side_effects()

virtual void value_sett::apply_assign_side_effects ( const exprt & lhs,

const exprt & rhs,

const namespacet &

)

inlineprivatevirtual

Subclass customisation point to apply global side-effects to this domain, after RHS values are read but before they are written.

For example, this is used in a recency-analysis plugin to demote existing most-recent objects to general case ones.

Definition at line 513 of file value_set.h.

◆ apply_code()

void value_sett::apply_code ( const codet & code,

const namespacet & ns

)

inline

Transforms this value-set by executing a given statement against it.

For example, assignment statements will update valuest by reading the value-set corresponding to their right-hand side and assigning it to their LHS.

Parameters: code instruction to apply

ns global namespace

Definition at line 323 of file value_set.h.

◆ apply_code_rec()

void value_sett::apply_code_rec ( const codet & code,

const namespacet & ns

)

protectedvirtual

Subclass customisation point for applying code to this domain:

Definition at line 1845 of file value_set.cpp.

◆ assign()

void value_sett::assign ( const exprt & lhs,

const exprt & rhs,

const namespacet & ns,

bool is_simplified,

bool add_to_sets

)

Transforms this value-set by executing executing the assignment lhs := rhs against it.

Parameters: lhs written expression

rhs read expression

ns global namespace

is_simplified if false, simplify will be used to simplify RHS and LHS before execution. If you know they are already simplified, set this to save a little time.

add_to_sets if true, execute a weak assignment (the LHS possible values are added to but not overwritten). Otherwise execute a strong (overwriting) assignment. Note the nature of lhs may internally prevent a strong assignment, as in x == y ? z : w := a, where either y or z MAY, but not MUST, be overwritten.

Definition at line 1499 of file value_set.cpp.

◆ assign_rec()

void value_sett::assign_rec ( const exprt & lhs,

const object_mapt & values_rhs,

const std::string & suffix,

const namespacet & ns,

bool add_to_sets

)

protectedvirtual

Subclass customisation point for recursion over LHS expression:

Do not take a reference to object_numbering's storage as we may call object_numbering.number(), which may reallocate it.

Definition at line 1654 of file value_set.cpp.

◆ clear()

void value_sett::clear ( )

inline

Definition at line 240 of file value_set.h.

◆ dereference_rec()

void value_sett::dereference_rec ( const exprt & src,

exprt & dest

) const

protected

Sets dest to src with any wrapping typecasts removed.

Definition at line 1307 of file value_set.cpp.

◆ do_end_function()

void value_sett::do_end_function ( const exprt & lhs,

const namespacet & ns

)

Transforms this value-set by assigning this function's return value to a given LHS expression.

Note this has no effect if remove_returns has been run, in which case returns are explicitly passed via global variables named function_name#return_value and are handled via the usual apply_code path.

Parameters: lhs expression that receives the return value

ns global namespace

Definition at line 1833 of file value_set.cpp.

◆ do_function_call()

void value_sett::do_function_call ( const irep_idt & function,

const exprt::operandst & arguments,

const namespacet & ns

)

Transforms this value-set by executing the actual -> formal parameter assignments for a particular callee.

For example, for function f(int* x, void* y) and call f(&g, &h) this would execute assignments x := &g and y := &h.

Parameters: function function being called

arguments actual arguments

ns global namespace

Definition at line 1787 of file value_set.cpp.

◆ erase_struct_union_symbol()

void value_sett::erase_struct_union_symbol ( const struct_union_typet & struct_union_type,

const std::string & erase_prefix,

const namespacet & ns

)

protected

Definition at line 2032 of file value_set.cpp.

◆ erase_symbol()

void value_sett::erase_symbol ( const symbol_exprt & symbol_expr,

const namespacet & ns

)

Definition at line 2070 of file value_set.cpp.

◆ erase_symbol_rec()

void value_sett::erase_symbol_rec ( const typet & type,

const std::string & erase_prefix,

const namespacet & ns

)

protected

Definition at line 2052 of file value_set.cpp.

◆ erase_values_from_entry()

void value_sett::erase_values_from_entry ( const irep_idt & index,

const std::unordered_set< exprt, irep_hash > & values_to_erase

)

Update the entry stored at index by erasing any values listed in values_to_erase.

Parameters: index index in the value set

values_to_erase set of values to remove from the entry

Definition at line 1997 of file value_set.cpp.

◆ eval_pointer_offset()

bool value_sett::eval_pointer_offset ( exprt & expr,

const namespacet & ns

) const

Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-set's information.

For example, if expr contained POINTER_OFFSET(y), and this value set indicates y points to object z offset 4, then the expression will be replaced by constant 4. If we don't know where y points, or it may point to multiple distinct offsets, then the expression will be left alone.

Parameters: expr expression whose pointer offsets should be replaced

ns global namespace

Returns: true if any offset expression was successfully replaced.

Definition at line 335 of file value_set.cpp.

◆ field_sensitive()

bool value_sett::field_sensitive ( const irep_idt & id,

const typet & type

)

virtual

Determines whether an identifier of a given type should have its fields distinguished.

Virtual so that subclasses can override this behaviour.

Definition at line 43 of file value_set.cpp.

◆ find_entry()

const value_sett::entryt * value_sett::find_entry ( const irep_idt & id ) const

Finds an entry in this value-set.

The interface differs from update_entry because get_value_set_rec wants to check for a struct's first component before stripping the suffix as is done in update_entry.

Parameters: id identifier to find.

Returns: a constant pointer to an entry if found, or null otherwise.

Definition at line 55 of file value_set.cpp.

◆ get_index_of_symbol()

std::optional< irep_idt > value_sett::get_index_of_symbol ( irep_idt identifier,

const typet & type,

const std::string & suffix,

const namespacet & ns

) const

Get the index of the symbol and suffix.

Parameters: identifier The identifier for the symbol

type The type of the symbol

suffix The suffix for the entry

ns The global namespace, for following type if it is a struct tag type or a union tag type

Returns: The index if the symbol is known, else nullopt.

Definition at line 451 of file value_set.cpp.

◆ get_insert_action()

value_sett::insert_actiont value_sett::get_insert_action ( const object_mapt & dest,

object_numberingt::number_type n,

const offsett & offset

) const

Determines what would happen if object number n was inserted into map dest with offset offset – the possibilities being, nothing (the entry is already present), a new entry would be inserted (no existing entry with number n was found), or an existing entry's offset would be reset (indicating there is already an entry with number n, but with differing offset).

Definition at line 100 of file value_set.cpp.

◆ get_reference_set() [1/2]

void value_sett::get_reference_set ( const exprt & expr,

object_mapt & dest,

const namespacet & ns

) const

inlineprotected

See the other overload of get_reference_set.

This one returns object numbers and offsets instead of expressions.

Definition at line 433 of file value_set.h.

◆ get_reference_set() [2/2]

void value_sett::get_reference_set ( const exprt & expr,

value_setst::valuest & dest,

const namespacet & ns

) const

Gets the set of expressions that expr may refer to, according to this value set.

Note the contrast with get_value_set: if x holds a pointer to y, then get_value_set(x) includes y while get_reference_set(x) returns { x }.

Parameters: expr query expression

[out] dest overwritten with result expression set

ns global namespace

Definition at line 1322 of file value_set.cpp.

◆ get_reference_set_rec()

void value_sett::get_reference_set_rec ( const exprt & expr,

object_mapt & dest,

const namespacet & ns

) const

protected

See get_reference_set.

Definition at line 1337 of file value_set.cpp.

◆ get_value_set() [1/2]

std::vector< exprt > value_sett::get_value_set ( exprt expr,

const namespacet & ns

) const

Gets values pointed to by expr, including following dereference operators (i.e.

this is not a simple lookup in valuest).

Parameters: expr query expression

ns global namespace

Returns: list of expressions that expr may point to. These expressions are object_descriptor_exprt or have id ID_invalid or ID_unknown.

Definition at line 390 of file value_set.cpp.

◆ get_value_set() [2/2]

value_sett::object_mapt value_sett::get_value_set ( exprt expr,

const namespacet & ns,

bool is_simplified

) const

protected

Reads the set of objects pointed to by expr, including making recursive lookups for dereference operations etc.

Parameters: expr query expression

ns global namespace

is_simplified if false, simplify expr before reading.

Returns: the set of object numbers pointed to

Definition at line 397 of file value_set.cpp.

◆ get_value_set_rec()

void value_sett::get_value_set_rec ( const exprt & expr,

object_mapt & dest,

bool & includes_nondet_pointer,

const std::string & suffix,

const typet & original_type,

const namespacet & ns

) const

protectedvirtual

Subclass customisation point for recursion over RHS expression.

Parameters: expr RHS expression to get value set for.

[out] dest value set for expr.

[out] includes_nondet_pointer expr includes a non-deterministic value, and the caller may want to expand dest to reflect this.

suffix context to enable field sensitivity.

original_type type of expr when starting the recursion.

ns namespace.

Do not take a reference to object_numbering's storage as we may call object_numbering.number(), which may reallocate it.

Definition at line 505 of file value_set.cpp.

◆ guard()

void value_sett::guard ( const exprt & expr,

const namespacet & ns

)

Transforms this value-set by assuming an expression holds.

Currently this can only mark dynamic objects valid; all other assumptions are ignored.

Parameters: expr condition to assume

ns global namespace

Definition at line 1965 of file value_set.cpp.

◆ insert() [1/4]

bool value_sett::insert ( object_mapt & dest,

const exprt & expr,

const offsett & offset

) const

inline

Adds an expression and offset to an object map.

If the destination map has an existing element for the same expression with a differing offset its offset is marked unknown.

Parameters: dest object map to update

expr expression to add

offset offset into expr (may be unknown).

Definition at line 178 of file value_set.h.

◆ insert() [2/4]

bool value_sett::insert ( object_mapt & dest,

const exprt & src

) const

inline

Adds an expression to an object map, with unknown offset.

If the destination map has an existing element for the same expression its offset is marked unknown.

Parameters: dest object map to update

src expression to add

Definition at line 137 of file value_set.h.

◆ insert() [3/4]

bool value_sett::insert ( object_mapt & dest,

const object_map_dt::value_type & it

) const

inline

Merges an existing element into an object map.

If the destination map has an existing element for the same expression with a different offset its offset is marked unknown (so e.g. x -> 0 and x -> 1 merge into x -> ?).

Parameters: dest object map to update.

it iterator pointing to new element

Definition at line 127 of file value_set.h.

◆ insert() [4/4]

bool value_sett::insert ( object_mapt & dest,

object_numberingt::number_type n,

const offsett & offset

) const

Adds a numbered expression and offset to an object map.

If the destination map has an existing element for the same expression with a differing offset its offset is marked unknown.

Parameters: dest object map to update

n object number to add; must be mapped to the corresponding expression by object_numbering.

offset offset into object n (may be unknown).

Definition at line 120 of file value_set.cpp.

◆ make_union() [1/3]

bool value_sett::make_union ( const value_sett & new_values )

inline

Merges an entire existing value_sett's data into this one.

Returns: true if anything changed.

Definition at line 303 of file value_set.h.

◆ make_union() [2/3]

bool value_sett::make_union ( const valuest & new_values )

Merges an entire existing value_sett's data into this one.

Parameters: new_values new values to merge in

Returns: true if anything changed.

Definition at line 270 of file value_set.cpp.

◆ make_union() [3/3]

bool value_sett::make_union ( object_mapt & dest,

const object_mapt & src

) const

Merges two RHS expression sets.

Parameters: [in,out] dest set to merge into

src set to merge in

Returns: true if anything changed.

Definition at line 320 of file value_set.cpp.

◆ make_union_would_change()

bool value_sett::make_union_would_change ( const object_mapt & dest,

const object_mapt & src

) const

Determines whether merging two RHS expression sets would cause any change.

Parameters: dest set that would be merged into

src set that would be merged in

Returns: true if anything changed.

Definition at line 302 of file value_set.cpp.

◆ operator=() [1/2]

value_sett & value_sett::operator= ( const value_sett & other )

delete

◆ operator=() [2/2]

value_sett & value_sett::operator= ( value_sett && other )

inline

Definition at line 60 of file value_set.h.

◆ output()

void value_sett::output ( std::ostream & out,

const std::string & indent = ""

) const

Pretty-print this value-set.

Parameters: [out] out stream to write to

indent string to use for indentation of the output

Definition at line 138 of file value_set.cpp.

◆ output_xml()

xmlt value_sett::output_xml ( void ) const

Output the value set formatted as XML.

Definition at line 217 of file value_set.cpp.

◆ set()

void value_sett::set ( object_mapt & dest,

const object_map_dt::value_type & it

) const

inline

Sets an element in object map dest to match an existing element it from a different map.

Any existing element for the same exprt is overwritten.

Parameters: dest object map to update.

it iterator pointing to new element

Definition at line 116 of file value_set.h.

◆ to_expr()

exprt value_sett::to_expr ( const object_map_dt::value_type & it ) const

Converts an object_map_dt element object_number -> offset into an object_descriptor_exprt with .object() == object_numbering.at(object_number) and .offset() == offset.

Definition at line 250 of file value_set.cpp.

◆ update_entry()

void value_sett::update_entry ( const entryt & e,

const typet & type,

const object_mapt & new_values,

bool add_to_sets

)

Adds or replaces an entry in this value-set.

Parameters: e entry to find. Its id and suffix fields will be used to find a corresponding entry; if a fresh entry is created its object_map (RHS value set) will be merged with or replaced by new_values, depending on the value of add_to_sets. If an entry already exists, the object map of e is ignored.

type type of e.identifier, used to determine whether e's suffix should be used to find a field-sensitive value-set or whether a single entry should be shared by all of symbol e.identifier.

new_values values to be stored for the entry.

add_to_sets if true, merge in new_values instead of replacing the existing values.

Definition at line 61 of file value_set.cpp.

Member Data Documentation

◆ empty_object_map

const value_sett::object_map_dt value_sett::empty_object_map {}

static

Definition at line 40 of file value_set.h.

◆ location_number

unsigned value_sett::location_number

Matches the location_number field of the instruction that corresponds to this value_sett instance in value_set_domaint's state map.

Definition at line 72 of file value_set.h.

◆ object_numbering

object_numberingt value_sett::object_numbering

static

Global shared object numbering, used to abbreviate expressions stored in value sets.

Definition at line 76 of file value_set.h.

◆ values

valuest value_sett::values

Stores the LHS ID -> RHS expression set map.

See valuest documentation for more detail.

Definition at line 281 of file value_set.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set.h
/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set.cpp

value_sett
Generated by doxygen 1.9.8