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;
60std::vector<gdb_value_extractort::memory_scopet>::iterator
66 [&name](
const memory_scopet &scope) { return scope.id() == name; });
69std::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)
116 symbol.
type.
id() != ID_pointer ||
136 symbol_value.
address, symbol_size,
id);
141 for(
const auto &
id : symbols)
159 const exprt target_expr =
201 symbolt snapshot_symbol(symbol);
202 snapshot_symbol.
value = pair.second;
204 snapshot.
insert(snapshot_symbol);
210 const symbolt &symbol = pair.second;
236 auto it =
values.find(memory_location);
256 values.insert(std::make_pair(memory_location, new_symbol));
279 const auto &memory_location = pointer_value.
address;
280 std::string memory_location_string = memory_location.
string();
284 std::string struct_name;
288 std::string member_offset_string;
290 pointer_value.
pointee,
'+', struct_name, member_offset_string,
true);
295 struct_name = pointer_value.
pointee;
308 const auto &struct_symbol_expr = struct_symbol->
symbol_expr();
309 if(struct_symbol->
type.
id() == ID_array)
317 if(struct_symbol->
type.
id() == ID_pointer)
331 maybe_member_expr.has_value(),
"structure doesn't have member");
336 return *maybe_member_expr;
348 const auto &function_name = pointer_value.
pointee;
351 if(function_symbol ==
nullptr)
354 "input source code does not contain function: " + function_name};
357 return function_symbol->symbol_expr();
367 const auto &memory_location = value.
address;
370 auto it =
values.find(memory_location);
379 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
380 return pointee_symbol_expr;
400 const auto number_of_elements = allocated_size /
get_type_size(target_type);
401 if(allocated_size != 1 && number_of_elements > 1)
405 for(
size_t i = 0; i < number_of_elements; i++)
411 elements.push_back(sub_expr_value);
416 const typet target_array_type =
423 const auto array_symbol =
429 values[memory_location] = array_symbol;
440 const exprt target_expr =
445 values[memory_location] = new_symbol;
451 const auto &known_value = it->second;
455 if(known_value.is_not_nil() && known_value.type() != expected_type)
471 if(pointer_value.
pointee.empty())
475 if(maybe_pointee.has_value())
476 pointer_value.
pointee = *maybe_pointee;
477 if(pointer_value.
pointee.find(
"+") != std::string::npos)
482 if(pointee_symbol ==
nullptr)
484 const auto &pointee_type = pointee_symbol->
type;
485 return pointee_type.
id() == ID_struct_tag ||
486 pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
487 pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
492 const exprt &zero_expr,
501 const auto known_pointer =
memory_map.find(c_expr);
504 known_pointer->second.pointee == c_expr)
506 : known_pointer->second;
510 const auto memory_location = value.
address;
512 if(!memory_location.is_null())
517 const auto target_expr =
522 return std::move(result_expr);
528 const auto target_expr =
533 return std::move(result_expr);
537 const auto target_expr =
543 if(target_expr.is_nil())
553 if(target_expr.type().id() == ID_array)
558 if(result_indexed_expr->type() == zero_expr.
type())
559 return *result_indexed_expr;
562 return std::move(result_expr);
566 if(target_expr.type() == zero_expr.
type())
571 if(result_expr.type() != zero_expr.
type())
573 return std::move(result_expr);
589 exprt new_array(array);
591 for(
size_t i = 0; i < new_array.
operands().size(); ++i)
605 const exprt &zero_expr,
619 if(!maybe_value.has_value())
621 const std::string value = *maybe_value;
634 if(!maybe_value.has_value() || maybe_value->empty())
636 const std::string value = *maybe_value;
641 else if(type.
id() == ID_c_bool)
647 if(!maybe_value.has_value())
649 const std::string value = *maybe_value;
653 else if(type.
id() == ID_c_enum)
659 if(!maybe_value.has_value())
661 const std::string value = *maybe_value;
665 else if(type.
id() == ID_struct_tag)
669 else if(type.
id() == ID_array)
673 else if(type.
id() == ID_pointer)
679 else if(type.
id() == ID_union_tag)
688 const exprt &zero_expr,
696 exprt new_expr(zero_expr);
701 for(
size_t i = 0; i < new_expr.
operands().size(); ++i)
721 const exprt &zero_expr,
729 exprt new_expr(zero_expr);
736 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.
const typet & element_type() const
The type of the elements of the array.
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
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
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.
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.
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.
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.
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.
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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 > 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)
#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(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