26 const std::vector<std::string> &args)
28 symbol_table(symbol_table),
55 auto point_int = address2size_t(point);
57 return (point_int - begin_int) / member_size;
60 std::vector<gdb_value_extractort::memory_scopet>::iterator
66 [&name](
const memory_scopet &scope) { return scope.id() == name; });
69 std::vector<gdb_value_extractort::memory_scopet>::iterator
76 return memory_scope.contains(point);
86 return scope_it->size();
97 const auto pointer_distance = scope_it->distance(point, member_size);
99 (pointer_distance > 0 ?
"+" +
integer2string(pointer_distance) :
"");
106 return *maybe_size / CHAR_BIT;
110 const std::list<std::string> &symbols)
113 for(
const auto &
id : symbols)
117 symbol.
type.
id() != ID_pointer ||
137 symbol_value.
address, symbol_size,
id);
142 for(
const auto &
id : symbols)
160 const exprt target_expr =
202 symbolt snapshot_symbol(symbol);
203 snapshot_symbol.
value = pair.second;
205 snapshot.
insert(snapshot_symbol);
211 const symbolt &symbol = pair.second;
237 auto it =
values.find(memory_location);
257 values.insert(std::make_pair(memory_location, new_symbol));
280 const auto &memory_location = pointer_value.
address;
281 std::string memory_location_string = memory_location.
string();
285 std::string struct_name;
289 std::string member_offset_string;
291 pointer_value.
pointee,
'+', struct_name, member_offset_string,
true);
296 struct_name = pointer_value.
pointee;
309 const auto &struct_symbol_expr = struct_symbol->
symbol_expr();
310 if(struct_symbol->
type.
id() == ID_array)
318 if(struct_symbol->
type.
id() == ID_pointer)
332 maybe_member_expr.has_value(),
"structure doesn't have member");
337 return *maybe_member_expr;
349 const auto &function_name = pointer_value.
pointee;
352 if(function_symbol ==
nullptr)
355 "input source code does not contain function: " + function_name};
358 return function_symbol->symbol_expr();
368 const auto &memory_location = value.
address;
371 auto it =
values.find(memory_location);
380 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
381 return pointee_symbol_expr;
401 const auto number_of_elements = allocated_size /
get_type_size(target_type);
402 if(allocated_size != 1 && number_of_elements > 1)
406 for(
size_t i = 0; i < number_of_elements; i++)
412 elements.push_back(sub_expr_value);
417 const typet target_array_type =
424 const auto array_symbol =
430 values[memory_location] = array_symbol;
441 const exprt target_expr =
446 values[memory_location] = new_symbol;
452 const auto &known_value = it->second;
456 if(known_value.is_not_nil() && known_value.type() != expected_type)
472 if(pointer_value.
pointee.empty())
476 if(maybe_pointee.has_value())
477 pointer_value.
pointee = *maybe_pointee;
478 if(pointer_value.
pointee.find(
"+") != std::string::npos)
483 if(pointee_symbol ==
nullptr)
485 const auto &pointee_type = pointee_symbol->
type;
486 return pointee_type.
id() == ID_struct_tag ||
487 pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
488 pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
493 const exprt &zero_expr,
502 const auto known_pointer =
memory_map.find(c_expr);
505 known_pointer->second.pointee == c_expr)
507 : known_pointer->second;
511 const auto memory_location = value.
address;
513 if(!memory_location.is_null())
518 const auto target_expr =
523 return std::move(result_expr);
529 const auto target_expr =
534 return std::move(result_expr);
538 const auto target_expr =
544 if(target_expr.is_nil())
554 if(target_expr.type().id() == ID_array)
559 if(result_indexed_expr->type() == zero_expr.
type())
560 return *result_indexed_expr;
563 return std::move(result_expr);
567 if(target_expr.type() == zero_expr.
type())
572 if(result_expr.type() != zero_expr.
type())
574 return std::move(result_expr);
590 exprt new_array(array);
592 for(
size_t i = 0; i < new_array.
operands().size(); ++i)
606 const exprt &zero_expr,
620 if(!maybe_value.has_value())
622 const std::string value = *maybe_value;
635 if(!maybe_value.has_value() || maybe_value->empty())
637 const std::string value = *maybe_value;
642 else if(type.
id() == ID_c_bool)
648 if(!maybe_value.has_value())
650 const std::string value = *maybe_value;
654 else if(type.
id() == ID_c_enum)
660 if(!maybe_value.has_value())
662 const std::string value = *maybe_value;
666 else if(type.
id() == ID_struct_tag)
670 else if(type.
id() == ID_array)
674 else if(type.
id() == ID_pointer)
680 else if(type.
id() == ID_union_tag)
689 const exprt &zero_expr,
697 exprt new_expr(zero_expr);
702 for(
size_t i = 0; i < new_expr.
operands().size(); ++i)
708 "struct member must not be of code type");
725 const exprt &zero_expr,
733 exprt new_expr(zero_expr);
740 auto &operand = new_expr.
operands()[0];
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.
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.
const typet & element_type() const
The type of the elements of the array.
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
void add(const codet &code)
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
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
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.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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 typet & base_type() const
The type of the data what we point to.
const array_typet & type() const
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
const componentst & components() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
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.
const symbolt & lookup_ref(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.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
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.
exprt value
Initial value 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< 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)
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, 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)
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::size_t safe_string2size_t(const std::string &str, int base)
void split_string(const std::string &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 string() const
std::string address_string
Data associated with the value of a pointer, i.e.
std::optional< std::string > string
bool has_known_offset() const