26 const std::vector<std::string> &args)
57mp_integer gdb_value_extractort::memory_scopet::distance(
61 auto point_int = address2size_t(point);
63 return (point_int - begin_int) / member_size;
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);
92 return scope_it->size();
95std::optional<std::string> gdb_value_extractort::get_malloc_pointee(
103 const auto pointer_distance = scope_it->distance(point, member_size);
105 (pointer_distance > 0 ?
"+" +
integer2string(pointer_distance) :
"");
112 return *maybe_size / CHAR_BIT;
116 const std::list<std::string> &symbols)
119 for(
const auto &
id : symbols)
123 symbol.
type.
id() != ID_pointer ||
129 const std::string c_expr =
c_converter.convert(aoe);
139 size_t symbol_size =
gdb_api.query_malloc_size(c_symbol);
143 symbol_value.
address, symbol_size,
id);
148 for(
const auto &
id : symbols)
156 const symbolt &symbol =
ns.lookup(symbol_name);
166 const exprt target_expr =
208 symbolt snapshot_symbol(symbol);
209 snapshot_symbol.
value = pair.second;
211 snapshot.
insert(snapshot_symbol);
217 const symbolt &symbol = pair.second;
243 auto it =
values.find(memory_location);
263 values.insert(std::make_pair(memory_location, new_symbol));
286 const auto &memory_location = pointer_value.
address;
287 std::string memory_location_string = memory_location.
string();
291 std::string struct_name;
295 std::string member_offset_string;
297 pointer_value.
pointee,
'+', struct_name, member_offset_string,
true);
302 struct_name = pointer_value.
pointee;
315 const auto &struct_symbol_expr = struct_symbol->
symbol_expr();
316 if(struct_symbol->
type.
id() == ID_array)
324 if(struct_symbol->
type.
id() == ID_pointer)
338 maybe_member_expr.has_value(),
"structure doesn't have member");
343 return *maybe_member_expr;
355 const auto &function_name = pointer_value.
pointee;
357 const auto function_symbol =
symbol_table.lookup(function_name);
358 if(function_symbol ==
nullptr)
361 "input source code does not contain function: " + function_name};
364 return function_symbol->symbol_expr();
374 const auto &memory_location = value.
address;
377 auto it =
values.find(memory_location);
386 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
387 return pointee_symbol_expr;
407 const auto number_of_elements = allocated_size /
get_type_size(target_type);
408 if(allocated_size != 1 && number_of_elements > 1)
412 for(
size_t i = 0; i < number_of_elements; i++)
418 elements.push_back(sub_expr_value);
423 const typet target_array_type =
430 const auto array_symbol =
436 values[memory_location] = array_symbol;
447 const exprt target_expr =
452 values[memory_location] = new_symbol;
458 const auto &known_value = it->second;
462 if(known_value.is_not_nil() && known_value.type() != expected_type)
478 if(pointer_value.
pointee.empty())
480 const auto maybe_pointee = get_malloc_pointee(
482 if(maybe_pointee.has_value())
483 pointer_value.
pointee = *maybe_pointee;
484 if(pointer_value.
pointee.find(
"+") != std::string::npos)
489 if(pointee_symbol ==
nullptr)
491 const auto &pointee_type = pointee_symbol->
type;
492 return pointee_type.
id() == ID_struct_tag ||
493 pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
494 pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
499 const exprt &zero_expr,
508 const auto known_pointer =
memory_map.find(c_expr);
511 known_pointer->second.pointee == c_expr)
513 : known_pointer->second;
517 const auto memory_location = value.
address;
519 if(!memory_location.is_null())
524 const auto target_expr =
529 return std::move(result_expr);
535 const auto target_expr =
540 return std::move(result_expr);
544 const auto target_expr =
550 if(target_expr.is_nil())
560 if(target_expr.type().id() == ID_array)
565 if(result_indexed_expr->type() == zero_expr.
type())
566 return *result_indexed_expr;
569 return std::move(result_expr);
573 if(target_expr.type() == zero_expr.
type())
578 if(result_expr.
type() != zero_expr.
type())
580 return std::move(result_expr);
596 exprt new_array(array);
598 for(
size_t i = 0; i < new_array.
operands().size(); ++i)
612 const exprt &zero_expr,
625 const auto maybe_value =
gdb_api.get_value(c_expr);
626 if(!maybe_value.has_value())
628 const std::string value = *maybe_value;
640 const auto maybe_value =
gdb_api.get_value(c_expr);
641 if(!maybe_value.has_value() || maybe_value->empty())
643 const std::string value = *maybe_value;
648 else if(type.
id() == ID_c_bool)
653 const auto maybe_value =
gdb_api.get_value(c_expr);
654 if(!maybe_value.has_value())
656 const std::string value = *maybe_value;
660 else if(type.
id() == ID_c_enum)
665 const auto maybe_value =
gdb_api.get_value(c_expr);
666 if(!maybe_value.has_value())
668 const std::string value = *maybe_value;
672 else if(type.
id() == ID_struct_tag)
676 else if(type.
id() == ID_array)
680 else if(type.
id() == ID_pointer)
686 else if(type.
id() == ID_union_tag)
695 const exprt &zero_expr,
703 exprt new_expr(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,
739 exprt new_expr(zero_expr);
742 const union_typet &union_type =
ns.follow_tag(union_tag_type);
746 auto &operand = new_expr.
operands()[0];
763 const auto maybe_value =
gdb_api.get_value(c_expr);
High-level interface to gdb.
unsignedbv_typet size_type()
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.
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.
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.
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 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).
void identifier(const irep_idt &identifier)
The symbol table base class interface.
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< 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.
std::string string() const
std::string address_string
std::optional< std::string > string
bool has_known_offset() const