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;
112 for(
const auto &
id : symbols)
134 symbol_value.
address, symbol_size,
id);
139 for(
const auto &
id : symbols)
157 const exprt target_expr =
199 symbolt snapshot_symbol(symbol);
200 snapshot_symbol.
value = pair.second;
202 snapshot.
insert(snapshot_symbol);
208 const symbolt &symbol = pair.second;
234 auto it =
values.find(memory_location);
254 values.insert(std::make_pair(memory_location, new_symbol));
273 const auto &memory_location = pointer_value.
address;
274 std::string memory_location_string = memory_location.
string();
278 std::string struct_name;
282 std::string member_offset_string;
284 pointer_value.
pointee,
'+', struct_name, member_offset_string,
true);
289 struct_name = pointer_value.
pointee;
302 const auto &struct_symbol_expr = struct_symbol->
symbol_expr();
303 if(struct_symbol->
type.
id() == ID_array)
310 if(struct_symbol->
type.
id() == ID_pointer)
321 maybe_member_expr.has_value(),
"structure doesn't have member");
325 return *maybe_member_expr;
337 const auto &function_name = pointer_value.
pointee;
340 if(function_symbol ==
nullptr)
343 "input source code does not contain function: " + function_name};
346 return function_symbol->symbol_expr();
356 const auto &memory_location = value.
address;
359 auto it =
values.find(memory_location);
368 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
369 return pointee_symbol_expr;
389 const auto number_of_elements = allocated_size /
get_type_size(target_type);
390 if(allocated_size != 1 && number_of_elements > 1)
394 for(
size_t i = 0; i < number_of_elements; i++)
400 elements.push_back(sub_expr_value);
405 const typet target_array_type =
412 const auto array_symbol =
418 values[memory_location] = array_symbol;
429 const exprt target_expr =
434 values[memory_location] = new_symbol;
440 const auto &known_value = it->second;
444 if(known_value.is_not_nil() && known_value.type() != expected_type)
455 const typet &expected_type)
460 if(pointer_value.
pointee.empty())
464 if(maybe_pointee.has_value())
465 pointer_value.
pointee = *maybe_pointee;
466 if(pointer_value.
pointee.find(
"+") != std::string::npos)
471 if(pointee_symbol ==
nullptr)
473 const auto &pointee_type = pointee_symbol->
type;
474 return pointee_type.
id() == ID_struct_tag ||
475 pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
476 pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
481 const exprt &zero_expr,
490 const auto known_pointer =
memory_map.find(c_expr);
493 known_pointer->second.pointee == c_expr)
495 : known_pointer->second;
499 const auto memory_location = value.
address;
501 if(!memory_location.is_null())
506 const auto target_expr =
511 return std::move(result_expr);
517 const auto target_expr =
522 return std::move(result_expr);
526 const auto target_expr =
532 if(target_expr.is_nil())
542 if(target_expr.type().id() == ID_array)
547 if(result_indexed_expr->type() == zero_expr.
type())
548 return *result_indexed_expr;
551 return std::move(result_expr);
555 if(target_expr.type() == zero_expr.
type())
560 if(result_expr.type() != zero_expr.
type())
562 return std::move(result_expr);
578 exprt new_array(array);
580 for(
size_t i = 0; i < new_array.
operands().size(); ++i)
594 const exprt &zero_expr,
608 if(!maybe_value.has_value())
610 const std::string value = *maybe_value;
623 if(!maybe_value.has_value() || maybe_value->empty())
625 const std::string value = *maybe_value;
630 else if(type.
id() == ID_c_bool)
636 if(!maybe_value.has_value())
638 const std::string value = *maybe_value;
642 else if(type.
id() == ID_c_enum)
648 if(!maybe_value.has_value())
650 const std::string value = *maybe_value;
654 else if(type.
id() == ID_struct_tag)
658 else if(type.
id() == ID_array)
662 else if(type.
id() == ID_pointer)
668 else if(type.
id() == ID_union_tag)
677 const exprt &zero_expr,
685 exprt new_expr(zero_expr);
690 for(
size_t i = 0; i < new_expr.
operands().size(); ++i)
710 const exprt &zero_expr,
718 exprt new_expr(zero_expr);
725 auto &operand = new_expr.
operands()[0];
High-level interface to gdb.
bitvector_typet index_type()
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
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.
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
void add(const codet &code)
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.
optionalt< std::string > get_value(const std::string &expr)
Get the memory address pointed to by the given pointer expression.
size_t query_malloc_size(const std::string &pointer_expr)
Get the exact allocated size for a pointer pointer_expr.
pointer_valuet get_memory(const std::string &expr)
Get the value of a pointer associated with expr.
std::string what() const override
A human readable description of what went wrong.
Thrown when we can't handle something in an input source file.
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.
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
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.
const typet & subtype() const
A union tag type, i.e., union_typet with an identifier.
optionalt< 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)
nonstd::optional< T > optionalt
API to expression classes for Pointers.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, 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.
bool has_known_offset() const
optionalt< std::string > string