26 const std::vector<std::string> &args)
51mp_integer gdb_value_extractort::memory_scopet::distance(
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();
89std::optional<std::string> gdb_value_extractort::get_malloc_pointee(
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 ||
123 const std::string c_expr =
c_converter.convert(aoe);
133 size_t symbol_size =
gdb_api.query_malloc_size(c_symbol);
137 symbol_value.
address, symbol_size,
id);
142 for(
const auto &
id : symbols)
150 const symbolt &symbol =
ns.lookup(symbol_name);
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;
351 const auto function_symbol =
symbol_table.lookup(function_name);
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())
474 const auto maybe_pointee = get_malloc_pointee(
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,
619 const auto maybe_value =
gdb_api.get_value(c_expr);
620 if(!maybe_value.has_value())
622 const std::string value = *maybe_value;
634 const auto maybe_value =
gdb_api.get_value(c_expr);
635 if(!maybe_value.has_value() || maybe_value->empty())
637 const std::string value = *maybe_value;
642 else if(type.
id() == ID_c_bool)
647 const auto maybe_value =
gdb_api.get_value(c_expr);
648 if(!maybe_value.has_value())
650 const std::string value = *maybe_value;
654 else if(type.
id() == ID_c_enum)
659 const auto maybe_value =
gdb_api.get_value(c_expr);
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);
736 const union_typet &union_type =
ns.follow_tag(union_tag_type);
740 auto &operand = new_expr.
operands()[0];
757 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).
const irep_idt & get_identifier() const
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(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.
std::string string() const
std::string address_string
std::optional< std::string > string
bool has_known_offset() const