cprover
Loading...
Searching...
No Matches
analyze_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbol Analyzer
4
5Author: Malte Mues <mail.mues@gmail.com>
6 Daniel Poetzl
7
8\*******************************************************************/
9
10#include "analyze_symbol.h"
11
12#include <util/c_types.h>
13#include <util/c_types_util.h>
15#include <util/pointer_expr.h>
17#include <util/string2int.h>
19#include <util/string_utils.h>
20
21#include <climits>
22#include <cstdlib>
23
24gdb_value_extractort::gdb_value_extractort(
25 const symbol_table_baset &symbol_table,
26 const std::vector<std::string> &args)
27 : gdb_api(args),
28 symbol_table(symbol_table),
29 ns(symbol_table),
30 c_converter(ns, expr2c_configurationt::clean_configuration),
31 allocate_objects(ID_C, source_locationt(), irep_idt{}, this->symbol_table)
32{
33}
34
35gdb_value_extractort::memory_scopet::memory_scopet(
36 const memory_addresst &begin,
37 const mp_integer &byte_size,
38 const irep_idt &name)
39 : begin_int(safe_string2size_t(begin.address_string, 0)),
40 byte_size(byte_size),
41 name(name)
42{
43}
44
45size_t gdb_value_extractort::memory_scopet::address2size_t(
46 const memory_addresst &point) const
47{
48 return safe_string2size_t(point.address_string, 0);
49}
50
51mp_integer gdb_value_extractort::memory_scopet::distance(
52 const memory_addresst &point,
53 mp_integer member_size) const
54{
55 auto point_int = address2size_t(point);
56 CHECK_RETURN(check_containment(point_int));
57 return (point_int - begin_int) / member_size;
58}
59
60std::vector<gdb_value_extractort::memory_scopet>::iterator
61gdb_value_extractort::find_dynamic_allocation(irep_idt name)
62{
63 return std::find_if(
64 dynamically_allocated.begin(),
65 dynamically_allocated.end(),
66 [&name](const memory_scopet &scope) { return scope.id() == name; });
67}
68
69std::vector<gdb_value_extractort::memory_scopet>::iterator
70gdb_value_extractort::find_dynamic_allocation(const memory_addresst &point)
71{
72 return std::find_if(
73 dynamically_allocated.begin(),
74 dynamically_allocated.end(),
75 [&point](const memory_scopet &memory_scope) {
76 return memory_scope.contains(point);
77 });
78}
79
80mp_integer gdb_value_extractort::get_malloc_size(irep_idt name)
81{
82 const auto scope_it = find_dynamic_allocation(name);
83 if(scope_it == dynamically_allocated.end())
84 return 1;
85 else
86 return scope_it->size();
87}
88
89std::optional<std::string> gdb_value_extractort::get_malloc_pointee(
90 const memory_addresst &point,
91 mp_integer member_size)
92{
93 const auto scope_it = find_dynamic_allocation(point);
94 if(scope_it == dynamically_allocated.end())
95 return {};
96
97 const auto pointer_distance = scope_it->distance(point, member_size);
98 return id2string(scope_it->id()) +
99 (pointer_distance > 0 ? "+" + integer2string(pointer_distance) : "");
100}
101
102mp_integer gdb_value_extractort::get_type_size(const typet &type) const
103{
104 const auto maybe_size = pointer_offset_bits(type, ns);
105 CHECK_RETURN(maybe_size.has_value());
106 return *maybe_size / CHAR_BIT;
107}
108
109void gdb_value_extractort::analyze_symbols(
110 const std::list<std::string> &symbols)
111{
112 // record addresses of given symbols
113 for(const auto &id : symbols)
114 {
115 const symbolt &symbol = ns.lookup(id);
116 if(
117 symbol.type.id() != ID_pointer ||
119 {
120 const symbol_exprt &symbol_expr = ns.lookup(id).symbol_expr();
121 const address_of_exprt aoe(symbol_expr);
122
123 const std::string c_expr = c_converter.convert(aoe);
124 const pointer_valuet &value = gdb_api.get_memory(c_expr);
125 CHECK_RETURN(value.pointee.empty() || (id == value.pointee));
126
127 memory_map[id] = value;
128 }
129 else
130 {
131 const std::string c_symbol = c_converter.convert(symbol.symbol_expr());
132 const pointer_valuet &symbol_value = gdb_api.get_memory(c_symbol);
133 size_t symbol_size = gdb_api.query_malloc_size(c_symbol);
134
135 if(symbol_size > 1)
136 dynamically_allocated.emplace_back(
137 symbol_value.address, symbol_size, id);
138 memory_map[id] = symbol_value;
139 }
140 }
141
142 for(const auto &id : symbols)
143 {
144 analyze_symbol(id);
145 }
146}
147
148void gdb_value_extractort::analyze_symbol(const irep_idt &symbol_name)
149{
150 const symbolt &symbol = ns.lookup(symbol_name);
151 const symbol_exprt symbol_expr = symbol.symbol_expr();
152
153 try
154 {
155 const typet target_type = symbol.type;
156
157 const auto zero_expr = zero_initializer(target_type, symbol.location, ns);
158 CHECK_RETURN(zero_expr);
159
160 const exprt target_expr =
161 get_expr_value(symbol_expr, *zero_expr, symbol.location);
162
163 add_assignment(symbol_expr, target_expr);
164 }
165 catch(const gdb_interaction_exceptiont &e)
166 {
167 throw analysis_exceptiont(e.what());
168 }
169
170 process_outstanding_assignments();
171}
172
174std::string gdb_value_extractort::get_snapshot_as_c_code()
175{
176 code_blockt generated_code;
177
178 allocate_objects.declare_created_symbols(generated_code);
179
180 for(auto const &pair : assignments)
181 {
182 generated_code.add(code_assignt(pair.first, pair.second));
183 }
184
185 return c_converter.convert(generated_code);
186}
187
189symbol_tablet gdb_value_extractort::get_snapshot_as_symbol_table()
190{
191 symbol_tablet snapshot;
192
193 for(const auto &pair : assignments)
194 {
195 const symbol_exprt &symbol_expr = to_symbol_expr(pair.first);
196 const irep_idt id = symbol_expr.get_identifier();
197
198 INVARIANT(symbol_table.has_symbol(id), "symbol must exist in symbol table");
199
200 const symbolt &symbol = symbol_table.lookup_ref(id);
201
202 symbolt snapshot_symbol(symbol);
203 snapshot_symbol.value = pair.second;
204
205 snapshot.insert(snapshot_symbol);
206 }
207
208 // Also add type symbols to the snapshot
209 for(const auto &pair : symbol_table)
210 {
211 const symbolt &symbol = pair.second;
212
213 if(symbol.is_type)
214 {
215 snapshot.insert(symbol);
216 }
217 }
218
219 return snapshot;
220}
221
222void gdb_value_extractort::add_assignment(const exprt &lhs, const exprt &value)
223{
224 if(assignments.count(lhs) == 0)
225 assignments.emplace(std::make_pair(lhs, value));
226}
227
228exprt gdb_value_extractort::get_char_pointer_value(
229 const exprt &expr,
230 const memory_addresst &memory_location,
231 const source_locationt &location)
232{
233 PRECONDITION(expr.type().id() == ID_pointer);
235 PRECONDITION(!memory_location.is_null());
236
237 auto it = values.find(memory_location);
238
239 if(it == values.end())
240 {
241 std::string c_expr = c_converter.convert(expr);
242 pointer_valuet value = gdb_api.get_memory(c_expr);
243 CHECK_RETURN(value.string);
244
245 string_constantt init(*value.string);
246 CHECK_RETURN(to_array_type(init.type()).is_complete());
247
248 symbol_exprt dummy("tmp", pointer_type(init.type()));
249 code_blockt assignments;
250
251 const symbol_exprt new_symbol =
252 to_symbol_expr(allocate_objects.allocate_automatic_local_object(
253 assignments, dummy, init.type()));
254
255 add_assignment(new_symbol, init);
256
257 values.insert(std::make_pair(memory_location, new_symbol));
258
259 // check that we are returning objects of the right type
261 to_array_type(new_symbol.type()).element_type() ==
262 to_pointer_type(expr.type()).base_type());
263 return new_symbol;
264 }
265 else
266 {
268 to_array_type(it->second.type()).element_type() ==
269 to_pointer_type(expr.type()).base_type());
270 return it->second;
271 }
272}
273
274exprt gdb_value_extractort::get_pointer_to_member_value(
275 const exprt &expr,
276 const pointer_valuet &pointer_value,
277 const source_locationt &location)
278{
279 PRECONDITION(expr.type().id() == ID_pointer);
280 const auto &memory_location = pointer_value.address;
281 std::string memory_location_string = memory_location.string();
282 PRECONDITION(memory_location_string != "0x0");
283 PRECONDITION(!pointer_value.pointee.empty());
284
285 std::string struct_name;
286 size_t member_offset;
287 if(pointer_value.has_known_offset())
288 {
289 std::string member_offset_string;
291 pointer_value.pointee, '+', struct_name, member_offset_string, true);
292 member_offset = safe_string2size_t(member_offset_string);
293 }
294 else
295 {
296 struct_name = pointer_value.pointee;
297 member_offset = 0;
298 }
299
300 const symbolt *struct_symbol = symbol_table.lookup(struct_name);
301 DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
302
303 if(!has_known_memory_location(struct_name))
304 {
305 memory_map[struct_name] = gdb_api.get_memory(struct_name);
306 analyze_symbol(irep_idt{struct_name});
307 }
308
309 const auto &struct_symbol_expr = struct_symbol->symbol_expr();
310 if(struct_symbol->type.id() == ID_array)
311 {
312 return index_exprt{
313 struct_symbol_expr,
315 member_offset / get_type_size(to_pointer_type(expr.type()).base_type()),
316 c_index_type())};
317 }
318 if(struct_symbol->type.id() == ID_pointer)
319 {
320 return dereference_exprt{
321 plus_exprt{struct_symbol_expr,
323 expr.type()}};
324 }
325
326 const auto maybe_member_expr = get_subexpression_at_offset(
327 struct_symbol_expr,
330 ns);
332 maybe_member_expr.has_value(), "structure doesn't have member");
333
334 // check that we return the right type
336 maybe_member_expr->type() == to_pointer_type(expr.type()).base_type());
337 return *maybe_member_expr;
338}
339
340exprt gdb_value_extractort::get_pointer_to_function_value(
341 const exprt &expr,
342 const pointer_valuet &pointer_value,
343 const source_locationt &location)
344{
345 PRECONDITION(expr.type().id() == ID_pointer);
346 PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_code);
347 PRECONDITION(!pointer_value.address.is_null());
348
349 const auto &function_name = pointer_value.pointee;
350 CHECK_RETURN(!function_name.empty());
351 const auto function_symbol = symbol_table.lookup(function_name);
352 if(function_symbol == nullptr)
353 {
355 "input source code does not contain function: " + function_name};
356 }
357 CHECK_RETURN(function_symbol->type.id() == ID_code);
358 return function_symbol->symbol_expr();
359}
360
361exprt gdb_value_extractort::get_non_char_pointer_value(
362 const exprt &expr,
363 const pointer_valuet &value,
364 const source_locationt &location)
365{
366 PRECONDITION(expr.type().id() == ID_pointer);
368 const auto &memory_location = value.address;
369 PRECONDITION(!memory_location.is_null());
370
371 auto it = values.find(memory_location);
372
373 if(it == values.end())
374 {
375 if(!value.pointee.empty() && value.pointee != c_converter.convert(expr))
376 {
377 analyze_symbol(value.pointee);
378 const auto pointee_symbol = symbol_table.lookup(value.pointee);
379 CHECK_RETURN(pointee_symbol != nullptr);
380 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
381 return pointee_symbol_expr;
382 }
383
384 values.insert(std::make_pair(memory_location, nil_exprt()));
385
386 const typet target_type = to_pointer_type(expr.type()).base_type();
387
388 symbol_exprt dummy("tmp", expr.type());
389 code_blockt assignments;
390
391 const auto zero_expr = zero_initializer(target_type, location, ns);
392 CHECK_RETURN(zero_expr);
393
394 // Check if pointer was dynamically allocated (via malloc). If so we will
395 // replace the pointee with a static array filled with values stored at the
396 // expected positions. Since the allocated size is an over-approximation we
397 // may end up querying past the allocated bounds and building a larger array
398 // with meaningless values.
399 mp_integer allocated_size = get_malloc_size(c_converter.convert(expr));
400 // get the sizeof(target_type) and thus the number of elements
401 const auto number_of_elements = allocated_size / get_type_size(target_type);
402 if(allocated_size != 1 && number_of_elements > 1)
403 {
404 array_exprt::operandst elements;
405 // build the operands by querying for an index expression
406 for(size_t i = 0; i < number_of_elements; i++)
407 {
408 const auto sub_expr_value = get_expr_value(
410 *zero_expr,
411 location);
412 elements.push_back(sub_expr_value);
413 }
414 CHECK_RETURN(elements.size() == number_of_elements);
415
416 // knowing the number of elements we can build the type
417 const typet target_array_type =
418 array_typet{target_type, from_integer(elements.size(), c_index_type())};
419
420 array_exprt new_array{elements, to_array_type(target_array_type)};
421
422 // allocate a new symbol for the temporary static array
423 symbol_exprt array_dummy("tmp", pointer_type(target_array_type));
424 const auto array_symbol =
425 allocate_objects.allocate_automatic_local_object(
426 assignments, array_dummy, target_array_type);
427
428 // add assignment of value to newly created symbol
429 add_assignment(array_symbol, new_array);
430 values[memory_location] = array_symbol;
431 CHECK_RETURN(array_symbol.type().id() == ID_array);
432 return array_symbol;
433 }
434
435 const symbol_exprt new_symbol =
436 to_symbol_expr(allocate_objects.allocate_automatic_local_object(
437 assignments, dummy, target_type));
438
439 dereference_exprt dereference_expr(expr);
440
441 const exprt target_expr =
442 get_expr_value(dereference_expr, *zero_expr, location);
443 // add assignment of value to newly created symbol
444 add_assignment(new_symbol, target_expr);
445
446 values[memory_location] = new_symbol;
447
448 return new_symbol;
449 }
450 else
451 {
452 const auto &known_value = it->second;
453 const auto &expected_type = to_pointer_type(expr.type()).base_type();
454 if(find_dynamic_allocation(memory_location) != dynamically_allocated.end())
455 return known_value;
456 if(known_value.is_not_nil() && known_value.type() != expected_type)
457 {
458 return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
459 expected_type};
460 }
461 return known_value;
462 }
463}
464
465bool gdb_value_extractort::points_to_member(
466 pointer_valuet &pointer_value,
467 const pointer_typet &expected_type)
468{
469 if(pointer_value.has_known_offset())
470 return true;
471
472 if(pointer_value.pointee.empty())
473 {
474 const auto maybe_pointee = get_malloc_pointee(
475 pointer_value.address, get_type_size(expected_type.base_type()));
476 if(maybe_pointee.has_value())
477 pointer_value.pointee = *maybe_pointee;
478 if(pointer_value.pointee.find("+") != std::string::npos)
479 return true;
480 }
481
482 const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
483 if(pointee_symbol == nullptr)
484 return false;
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;
489}
490
491exprt gdb_value_extractort::get_pointer_value(
492 const exprt &expr,
493 const exprt &zero_expr,
494 const source_locationt &location)
495{
496 PRECONDITION(zero_expr.is_constant());
497
498 PRECONDITION(expr.type().id() == ID_pointer);
499 PRECONDITION(expr.type() == zero_expr.type());
500
501 std::string c_expr = c_converter.convert(expr);
502 const auto known_pointer = memory_map.find(c_expr);
503
504 pointer_valuet value = (known_pointer == memory_map.end() ||
505 known_pointer->second.pointee == c_expr)
506 ? gdb_api.get_memory(c_expr)
507 : known_pointer->second;
508 if(!value.valid)
509 return zero_expr;
510
511 const auto memory_location = value.address;
512
513 if(!memory_location.is_null())
514 {
515 // pointers-to-char can point to members as well, e.g. char[]
516 if(points_to_member(value, to_pointer_type(expr.type())))
517 {
518 const auto target_expr =
519 get_pointer_to_member_value(expr, value, location);
520 CHECK_RETURN(target_expr.is_not_nil());
521 const address_of_exprt result_expr{target_expr};
522 CHECK_RETURN(result_expr.type() == zero_expr.type());
523 return std::move(result_expr);
524 }
525
526 // pointer to function
527 if(to_pointer_type(expr.type()).base_type().id() == ID_code)
528 {
529 const auto target_expr =
530 get_pointer_to_function_value(expr, value, location);
531 CHECK_RETURN(target_expr.is_not_nil());
532 const address_of_exprt result_expr{target_expr};
533 CHECK_RETURN(result_expr.type() == zero_expr.type());
534 return std::move(result_expr);
535 }
536
537 // non-member: split for char/non-char
538 const auto target_expr =
540 ? get_char_pointer_value(expr, memory_location, location)
541 : get_non_char_pointer_value(expr, value, location);
542
543 // postpone if we cannot resolve now
544 if(target_expr.is_nil())
545 {
546 outstanding_assignments[expr] = memory_location;
547 return zero_expr;
548 }
549
550 // the pointee was (probably) dynamically allocated (but the allocation
551 // would not be visible in the snapshot) so we pretend it is statically
552 // allocated (we have the value) and return address to the first element
553 // of the array (instead of the array as char*)
554 if(target_expr.type().id() == ID_array)
555 {
556 const auto result_indexed_expr = get_subexpression_at_offset(
557 target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
558 CHECK_RETURN(result_indexed_expr.has_value());
559 if(result_indexed_expr->type() == zero_expr.type())
560 return *result_indexed_expr;
561 const address_of_exprt result_expr{*result_indexed_expr};
562 CHECK_RETURN(result_expr.type() == zero_expr.type());
563 return std::move(result_expr);
564 }
565
566 // if the types match return right away
567 if(target_expr.type() == zero_expr.type())
568 return target_expr;
569
570 // otherwise the address of target should type-match
571 const address_of_exprt result_expr{target_expr};
572 if(result_expr.type() != zero_expr.type())
573 return typecast_exprt{result_expr, zero_expr.type()};
574 return std::move(result_expr);
575 }
576
577 return zero_expr;
578}
579
580exprt gdb_value_extractort::get_array_value(
581 const exprt &expr,
582 const exprt &array,
583 const source_locationt &location)
584{
585 PRECONDITION(array.id() == ID_array);
586
587 PRECONDITION(expr.type().id() == ID_array);
588 PRECONDITION(expr.type() == array.type());
589
590 exprt new_array(array);
591
592 for(size_t i = 0; i < new_array.operands().size(); ++i)
593 {
594 const index_exprt index_expr(expr, from_integer(i, c_index_type()));
595
596 exprt &operand = new_array.operands()[i];
597
598 operand = get_expr_value(index_expr, operand, location);
599 }
600
601 return new_array;
602}
603
604exprt gdb_value_extractort::get_expr_value(
605 const exprt &expr,
606 const exprt &zero_expr,
607 const source_locationt &location)
608{
609 PRECONDITION(expr.type() == zero_expr.type());
610
611 const typet &type = expr.type();
612 PRECONDITION(type.id() != ID_struct);
613
614 if(is_c_integral_type(type))
615 {
616 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
617
618 std::string c_expr = c_converter.convert(expr);
619 const auto maybe_value = gdb_api.get_value(c_expr);
620 if(!maybe_value.has_value())
621 return zero_expr;
622 const std::string value = *maybe_value;
623
624 const mp_integer int_rep = string2integer(value);
625
626 return from_integer(int_rep, type);
627 }
628 else if(is_c_char_type(type))
629 {
630 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
631
632 // check the char-value and return as bitvector-type value
633 std::string c_expr = c_converter.convert(expr);
634 const auto maybe_value = gdb_api.get_value(c_expr);
635 if(!maybe_value.has_value() || maybe_value->empty())
636 return zero_expr;
637 const std::string value = *maybe_value;
638
639 const mp_integer int_rep = value[0];
640 return from_integer(int_rep, type);
641 }
642 else if(type.id() == ID_c_bool)
643 {
644 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
645
646 std::string c_expr = c_converter.convert(expr);
647 const auto maybe_value = gdb_api.get_value(c_expr);
648 if(!maybe_value.has_value())
649 return zero_expr;
650 const std::string value = *maybe_value;
651
652 return from_c_boolean_value(id2boolean(value), type);
653 }
654 else if(type.id() == ID_c_enum)
655 {
656 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
657
658 std::string c_expr = c_converter.convert(expr);
659 const auto maybe_value = gdb_api.get_value(c_expr);
660 if(!maybe_value.has_value())
661 return zero_expr;
662 const std::string value = *maybe_value;
663
665 }
666 else if(type.id() == ID_struct_tag)
667 {
668 return get_struct_value(expr, zero_expr, location);
669 }
670 else if(type.id() == ID_array)
671 {
672 return get_array_value(expr, zero_expr, location);
673 }
674 else if(type.id() == ID_pointer)
675 {
676 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
677
678 return get_pointer_value(expr, zero_expr, location);
679 }
680 else if(type.id() == ID_union_tag)
681 {
682 return get_union_value(expr, zero_expr, location);
683 }
685}
686
687exprt gdb_value_extractort::get_struct_value(
688 const exprt &expr,
689 const exprt &zero_expr,
690 const source_locationt &location)
691{
692 PRECONDITION(zero_expr.id() == ID_struct);
693
694 PRECONDITION(expr.type().id() == ID_struct_tag);
695 PRECONDITION(expr.type() == zero_expr.type());
696
697 exprt new_expr(zero_expr);
698
699 const struct_tag_typet &struct_tag_type = to_struct_tag_type(expr.type());
700 const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
701
702 for(size_t i = 0; i < new_expr.operands().size(); ++i)
703 {
704 const struct_typet::componentt &component = struct_type.components()[i];
705
707 component.type().id() != ID_code,
708 "struct member must not be of code type");
709 if(component.get_is_padding())
710 {
711 continue;
712 }
713
714 exprt &operand = new_expr.operands()[i];
715 member_exprt member_expr(expr, component);
716
717 operand = get_expr_value(member_expr, operand, location);
718 }
719
720 return new_expr;
721}
722
723exprt gdb_value_extractort::get_union_value(
724 const exprt &expr,
725 const exprt &zero_expr,
726 const source_locationt &location)
727{
728 PRECONDITION(zero_expr.id() == ID_union);
729
730 PRECONDITION(expr.type().id() == ID_union_tag);
731 PRECONDITION(expr.type() == zero_expr.type());
732
733 exprt new_expr(zero_expr);
734
735 const union_tag_typet &union_tag_type = to_union_tag_type(expr.type());
736 const union_typet &union_type = ns.follow_tag(union_tag_type);
737
738 CHECK_RETURN(new_expr.operands().size() == 1);
739 const union_typet::componentt &component = union_type.components()[0];
740 auto &operand = new_expr.operands()[0];
741 operand = get_expr_value(member_exprt{expr, component}, operand, location);
742 return new_expr;
743}
744
745void gdb_value_extractort::process_outstanding_assignments()
746{
747 for(const auto &pair : outstanding_assignments)
748 {
749 const address_of_exprt aoe(values[pair.second]);
750 add_assignment(pair.first, aoe);
751 }
752}
753
754std::string gdb_value_extractort::get_gdb_value(const exprt &expr)
755{
756 std::string c_expr = c_converter.convert(expr);
757 const auto maybe_value = gdb_api.get_value(c_expr);
758 CHECK_RETURN(maybe_value.has_value());
759 return *maybe_value;
760}
High-level interface to gdb.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
unsignedbv_typet size_type()
Definition c_types.cpp:50
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
bitvector_typet c_index_type()
Definition c_types.cpp:16
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
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.
Definition std_expr.h:1616
Arrays with given size.
Definition std_types.h:807
bool is_complete() const
Definition std_types.h:852
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition std_code.h:130
void add(const codet &code)
Definition std_code.h:168
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.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
Array index operator.
Definition std_expr.h:1465
Thrown when user-provided input cannot be processed.
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2841
The NIL expression.
Definition std_expr.h:3073
The plus expression Associativity is not specified.
Definition std_expr.h:1002
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.
Definition std_types.h:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
The symbol table base class interface.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
Semantic type conversion.
Definition std_expr.h:2068
The type of an expression, extends irept.
Definition type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:199
The union type.
Definition c_types.h:147
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)
Definition irep.h:44
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
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)
Pointer Logic.
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:80
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
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.
Definition expr2c.h:21