26 const std::vector<std::string> &args)
28 symbol_table(symbol_table),
54 std::string_view{
point.address_string}.substr(2), 16);
66std::vector<gdb_value_extractort::memory_scopet>::iterator
72 [&name](
const memory_scopet &scope) { return scope.id() == name; });
75std::vector<gdb_value_extractort::memory_scopet>::iterator
82 return memory_scope.contains(point);
116 const std::list<std::string> &symbols)
119 for(
const auto &
id : symbols)
148 for(
const auto &
id : symbols)
361 "input source code does not contain function: " + function_name};
430 const auto array_symbol =
499 const exprt &zero_expr,
598 for(
size_t i = 0; i <
new_array.operands().size(); ++i)
612 const exprt &zero_expr,
695 const exprt &zero_expr,
708 for(
size_t i = 0; i <
new_expr.operands().size(); ++i)
714 "struct member must not be of code type");
731 const exprt &zero_expr,
High-level interface to gdb.
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
This file contains functions, that should support test for underlying c types, in cases where this is...
bool is_c_integral_type(const typet &type)
This function checks, whether the type has been some kind of integer type in the c program.
bool id2boolean(const std::string &bool_value)
Convert id to a Boolean value.
constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
This function creates a constant representing either 0 or 1 as value of type type.
constant_exprt convert_member_name_to_enum_value(const irep_idt &member_name, const c_enum_typet &c_enum)
This function creates a constant representing the bitvector encoded integer value of a string in the ...
bool is_c_char_type(const typet &type)
This function checks, whether this has been a char type in the c program.
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Array constructor from list of elements.
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
virtual std::string what() const
A human readable description of what went wrong.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual std::string convert(const typet &src)
Base class for all expressions.
std::vector< exprt > operandst
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
std::optional< std::string > get_value(const std::string &expr)
Get the memory address pointed to by the given pointer expression.
pointer_valuet get_memory(const std::string &expr)
Get the value of a pointer associated with expr.
size_t query_malloc_size(const std::string &pointer_expr)
Get the exact allocated size for a pointer pointer_expr.
const irep_idt & id() const
Extract member of struct or union.
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const array_typet & type() const
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
Expression to hold a symbol (variable)
void identifier(const irep_idt &identifier)
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
Semantic type conversion.
The type of an expression, extends irept.
A union tag type, i.e., union_typet with an identifier.
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::size_t safe_string2size_t(std::string_view str, int base)
void split_string(std::string_view s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Used for configuring the behaviour of expr2c and type2c.
Memory address imbued with the explicit boolean data indicating if the address is null or not.
std::string address_string
Data associated with the value of a pointer, i.e.
std::optional< std::string > string