cprover
c_typecheck_base.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Conversion / Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "c_typecheck_base.h"
13
14#include <util/c_types.h>
15#include <util/config.h>
16#include <util/expr_util.h>
17#include <util/std_types.h>
18
19#include "ansi_c_declaration.h"
20#include "c_storage_spec.h"
21#include "expr2c.h"
22
23std::string c_typecheck_baset::to_string(const exprt &expr)
24{
25 return expr2c(expr, *this);
26}
27
28std::string c_typecheck_baset::to_string(const typet &type)
29{
30 return type2c(type, *this);
31}
32
34{
35 symbol.mode=mode;
36 symbol.module=module;
37
38 if(symbol_table.move(symbol, new_symbol))
39 {
41 error() << "failed to move symbol '" << symbol.name << "' into symbol table"
42 << eom;
43 throw 0;
44 }
45}
46
48{
49 bool is_function=symbol.type.id()==ID_code;
50
51 const typet &final_type=follow(symbol.type);
52
53 // set a few flags
54 symbol.is_lvalue=!symbol.is_type && !symbol.is_macro;
55
56 irep_idt root_name=symbol.base_name;
57 irep_idt new_name=symbol.name;
58
59 if(symbol.is_file_local)
60 {
61 // file-local stuff -- stays as is
62 // collisions are resolved during linking
63 }
64 else if(symbol.is_extern && !is_function)
65 {
66 // variables marked as "extern" go into the global namespace
67 // and have static lifetime
68 new_name=root_name;
69 symbol.is_static_lifetime=true;
70
71 if(symbol.value.is_not_nil())
72 {
73 // According to the C standard this should be an error, but at least some
74 // versions of Visual Studio insist to use this in their C library, and
75 // GCC just warns as well.
77 warning() << "`extern' symbol should not have an initializer" << eom;
78 }
79 }
80 else if(!is_function && symbol.value.id()==ID_code)
81 {
83 error() << "only functions can have a function body" << eom;
84 throw 0;
85 }
86
87 // set the pretty name
88 if(symbol.is_type && final_type.id() == ID_struct)
89 {
90 symbol.pretty_name="struct "+id2string(symbol.base_name);
91 }
92 else if(symbol.is_type && final_type.id() == ID_union)
93 {
94 symbol.pretty_name="union "+id2string(symbol.base_name);
95 }
96 else if(symbol.is_type && final_type.id() == ID_c_enum)
97 {
98 symbol.pretty_name="enum "+id2string(symbol.base_name);
99 }
100 else
101 {
102 symbol.pretty_name=new_name;
103 }
104
105 if(!symbol.is_type && !symbol.is_extern && symbol.type.id() == ID_empty)
106 {
107 error().source_location = symbol.location;
108 error() << "void-typed symbol not permitted" << eom;
109 throw 0;
110 }
111
112 // see if we have it already
113 symbol_tablet::symbolst::const_iterator old_it=
114 symbol_table.symbols.find(symbol.name);
115
116 if(old_it==symbol_table.symbols.end())
117 {
118 // just put into symbol_table
119 symbolt *new_symbol;
120 move_symbol(symbol, new_symbol);
121
122 typecheck_new_symbol(*new_symbol);
123 }
124 else
125 {
126 if(old_it->second.is_type!=symbol.is_type)
127 {
129 error() << "redeclaration of '" << symbol.display_name()
130 << "' as a different kind of symbol" << eom;
131 throw 0;
132 }
133
134 symbolt &existing_symbol = symbol_table.get_writeable_ref(symbol.name);
135 if(symbol.is_type)
136 typecheck_redefinition_type(existing_symbol, symbol);
137 else
138 typecheck_redefinition_non_type(existing_symbol, symbol);
139 }
140}
141
143{
144 if(symbol.is_parameter)
146
147 // check initializer, if needed
148
149 if(symbol.type.id()==ID_code)
150 {
151 if(symbol.value.is_not_nil() &&
152 !symbol.is_macro)
153 {
155 }
156 else
157 {
158 // we don't need the identifiers
159 for(auto &parameter : to_code_type(symbol.type).parameters())
160 parameter.set_identifier(irep_idt());
161 }
162 }
163 else if(!symbol.is_macro)
164 {
165 // check the initializer
166 do_initializer(symbol);
167 }
168}
169
171 symbolt &old_symbol,
172 symbolt &new_symbol)
173{
174 const typet &final_old=follow(old_symbol.type);
175 const typet &final_new=follow(new_symbol.type);
176
177 // see if we had something incomplete before
178 if(
179 (final_old.id() == ID_struct &&
180 to_struct_type(final_old).is_incomplete()) ||
181 (final_old.id() == ID_union && to_union_type(final_old).is_incomplete()) ||
182 (final_old.id() == ID_c_enum && to_c_enum_type(final_old).is_incomplete()))
183 {
184 // is the new one complete?
185 if(
186 final_new.id() == final_old.id() &&
187 ((final_new.id() == ID_struct &&
188 !to_struct_type(final_new).is_incomplete()) ||
189 (final_new.id() == ID_union &&
190 !to_union_type(final_new).is_incomplete()) ||
191 (final_new.id() == ID_c_enum &&
192 !to_c_enum_type(final_new).is_incomplete())))
193 {
194 // overwrite location
195 old_symbol.location=new_symbol.location;
196
197 // move body
198 old_symbol.type.swap(new_symbol.type);
199 }
200 else if(new_symbol.type.id()==old_symbol.type.id())
201 return; // ignore
202 else
203 {
204 error().source_location=new_symbol.location;
205 error() << "conflicting definition of type symbol '"
206 << new_symbol.display_name() << '\'' << eom;
207 throw 0;
208 }
209 }
210 else
211 {
212 // see if new one is just a tag
213 if(
214 (final_new.id() == ID_struct &&
215 to_struct_type(final_new).is_incomplete()) ||
216 (final_new.id() == ID_union &&
217 to_union_type(final_new).is_incomplete()) ||
218 (final_new.id() == ID_c_enum &&
219 to_c_enum_type(final_new).is_incomplete()))
220 {
221 if(final_old.id() == final_new.id())
222 {
223 // just ignore silently
224 }
225 else
226 {
227 // arg! new tag type
228 error().source_location=new_symbol.location;
229 error() << "conflicting definition of tag symbol '"
230 << new_symbol.display_name() << '\'' << eom;
231 throw 0;
232 }
233 }
235 final_new.id()==ID_c_enum && final_old.id()==ID_c_enum)
236 {
237 // under Windows, ignore this silently;
238 // MSC doesn't think this is a problem, but GCC complains.
239 }
240 else if(
242 final_new.id() == ID_pointer && final_old.id() == ID_pointer &&
243 follow(to_pointer_type(final_new).base_type()).id() == ID_c_enum &&
244 follow(to_pointer_type(final_old).base_type()).id() == ID_c_enum)
245 {
246 // under Windows, ignore this silently;
247 // MSC doesn't think this is a problem, but GCC complains.
248 }
249 else
250 {
251 // see if it changed
252 if(follow(new_symbol.type)!=follow(old_symbol.type))
253 {
254 error().source_location=new_symbol.location;
255 error() << "type symbol '" << new_symbol.display_name()
256 << "' defined twice:\n"
257 << "Original: " << to_string(old_symbol.type) << "\n"
258 << " New: " << to_string(new_symbol.type) << eom;
259 throw 0;
260 }
261 }
262 }
263}
264
266 symbolt &old_symbol,
267 symbolt &new_symbol)
268{
269 const typet &final_old=follow(old_symbol.type);
270 const typet &initial_new=follow(new_symbol.type);
271
272 if(
273 final_old.id() == ID_array &&
274 to_array_type(final_old).size().is_not_nil() &&
275 initial_new.id() == ID_array &&
276 to_array_type(initial_new).size().is_nil() &&
277 to_array_type(final_old).element_type() ==
278 to_array_type(initial_new).element_type())
279 {
280 // this is ok, just use old type
281 new_symbol.type=old_symbol.type;
282 }
283 else if(
284 final_old.id() == ID_array && to_array_type(final_old).size().is_nil() &&
285 initial_new.id() == ID_array &&
286 to_array_type(initial_new).size().is_not_nil() &&
287 to_array_type(final_old).element_type() ==
288 to_array_type(initial_new).element_type())
289 {
290 // update the type to enable the use of sizeof(x) on the
291 // right-hand side of a definition of x
292 old_symbol.type=new_symbol.type;
293 }
294
295 // do initializer, this may change the type
296 if(new_symbol.type.id() != ID_code && !new_symbol.is_macro)
297 do_initializer(new_symbol);
298
299 const typet &final_new=follow(new_symbol.type);
300
301 // K&R stuff?
302 if(old_symbol.type.id()==ID_KnR)
303 {
304 // check the type
305 if(final_new.id()==ID_code)
306 {
307 error().source_location=new_symbol.location;
308 error() << "function type not allowed for K&R function parameter"
309 << eom;
310 throw 0;
311 }
312
313 // fix up old symbol -- we now got the type
314 old_symbol.type=new_symbol.type;
315 return;
316 }
317
318 if(final_new.id()==ID_code)
319 {
320 if(final_old.id()!=ID_code)
321 {
322 error().source_location=new_symbol.location;
323 error() << "error: function symbol '" << new_symbol.display_name()
324 << "' redefined with a different type:\n"
325 << "Original: " << to_string(old_symbol.type) << "\n"
326 << " New: " << to_string(new_symbol.type) << eom;
327 throw 0;
328 }
329
330 code_typet &old_ct=to_code_type(old_symbol.type);
331 code_typet &new_ct=to_code_type(new_symbol.type);
332
333 const bool inlined = old_ct.get_inlined() || new_ct.get_inlined();
334
335 if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
336 old_ct=new_ct;
337 else if(!old_ct.has_ellipsis() && new_ct.has_ellipsis())
338 new_ct=old_ct;
339
340 if(inlined)
341 {
342 old_ct.set_inlined(true);
343 new_ct.set_inlined(true);
344 }
345
346 // do body
347
348 if(new_symbol.value.is_not_nil())
349 {
350 if(old_symbol.value.is_not_nil())
351 {
352 // gcc allows re-definition if the first
353 // definition is marked as "extern inline"
354
355 if(
356 old_ct.get_inlined() &&
361 {
362 // overwrite "extern inline" properties
363 old_symbol.is_extern=new_symbol.is_extern;
364 old_symbol.is_file_local=new_symbol.is_file_local;
365
366 // remove parameter declarations to avoid conflicts
367 for(const auto &old_parameter : old_ct.parameters())
368 {
369 const irep_idt &identifier = old_parameter.get_identifier();
370
371 symbol_tablet::symbolst::const_iterator p_s_it=
372 symbol_table.symbols.find(identifier);
373 if(p_s_it!=symbol_table.symbols.end())
374 symbol_table.erase(p_s_it);
375 }
376 }
377 else
378 {
379 error().source_location=new_symbol.location;
380 error() << "function body '" << new_symbol.display_name()
381 << "' defined twice" << eom;
382 throw 0;
383 }
384 }
385 else if(inlined)
386 {
387 // preserve "extern inline" properties
388 old_symbol.is_extern=new_symbol.is_extern;
389 old_symbol.is_file_local=new_symbol.is_file_local;
390 }
391 else if(new_symbol.is_weak)
392 {
393 // weak symbols
394 old_symbol.is_weak=true;
395 }
396
397 if(new_symbol.is_macro)
398 old_symbol.is_macro=true;
399 else
400 typecheck_function_body(new_symbol);
401
402 // overwrite location
403 old_symbol.location=new_symbol.location;
404
405 // move body
406 old_symbol.value.swap(new_symbol.value);
407
408 // overwrite type (because of parameter names)
409 old_symbol.type=new_symbol.type;
410 }
411
412 return;
413 }
414
415 if(final_old!=final_new)
416 {
417 if(
418 final_old.id() == ID_array && to_array_type(final_old).size().is_nil() &&
419 final_new.id() == ID_array &&
420 to_array_type(final_new).size().is_not_nil() &&
421 to_array_type(final_old).element_type() ==
422 to_array_type(final_new).element_type())
423 {
424 old_symbol.type=new_symbol.type;
425 }
426 else if(
427 final_old.id() == ID_pointer &&
428 to_pointer_type(final_old).base_type().id() == ID_code &&
429 to_code_type(to_pointer_type(final_old).base_type()).has_ellipsis() &&
430 final_new.id() == ID_pointer &&
431 to_pointer_type(final_new).base_type().id() == ID_code)
432 {
433 // to allow
434 // int (*f) ();
435 // int (*f) (int)=0;
436 old_symbol.type=new_symbol.type;
437 }
438 else if(
439 final_old.id() == ID_pointer &&
440 to_pointer_type(final_old).base_type().id() == ID_code &&
441 final_new.id() == ID_pointer &&
442 to_pointer_type(final_new).base_type().id() == ID_code &&
443 to_code_type(to_pointer_type(final_new).base_type()).has_ellipsis())
444 {
445 // to allow
446 // int (*f) (int)=0;
447 // int (*f) ();
448 }
449 else
450 {
451 error().source_location=new_symbol.location;
452 error() << "symbol '" << new_symbol.display_name()
453 << "' redefined with a different type:\n"
454 << "Original: " << to_string(old_symbol.type) << "\n"
455 << " New: " << to_string(new_symbol.type) << eom;
456 throw 0;
457 }
458 }
459 else // finals are equal
460 {
461 }
462
463 // do value
464 if(new_symbol.value.is_not_nil())
465 {
466 // see if we already have one
467 if(old_symbol.value.is_not_nil())
468 {
469 if(
470 new_symbol.is_macro && final_new.id() == ID_c_enum &&
471 old_symbol.value.is_constant() && new_symbol.value.is_constant() &&
472 old_symbol.value.get(ID_value) == new_symbol.value.get(ID_value))
473 {
474 // ignore
475 }
476 else
477 {
479 warning() << "symbol '" << new_symbol.display_name()
480 << "' already has an initial value" << eom;
481 }
482 }
483 else
484 {
485 old_symbol.value=new_symbol.value;
486 old_symbol.type=new_symbol.type;
487 old_symbol.is_macro=new_symbol.is_macro;
488 }
489 }
490
491 // take care of some flags
492 if(old_symbol.is_extern && !new_symbol.is_extern)
493 old_symbol.location=new_symbol.location;
494
495 old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern;
496
497 // We should likely check is_volatile and
498 // is_thread_local for consistency. GCC complains if these
499 // mismatch.
500}
501
503{
504 if(symbol.value.id() != ID_code)
505 {
506 error().source_location = symbol.location;
507 error() << "function '" << symbol.name << "' is initialized with "
508 << symbol.value.id() << eom;
509 throw 0;
510 }
511
512 code_typet &code_type = to_code_type(symbol.type);
513
514 // reset labels
515 labels_used.clear();
516 labels_defined.clear();
517
518 // fix type
519 symbol.value.type()=code_type;
520
521 // set return type
522 return_type=code_type.return_type();
523
524 unsigned anon_counter=0;
525
526 // Add the parameter declarations into the symbol table.
527 for(auto &p : code_type.parameters())
528 {
529 // may be anonymous
530 if(p.get_base_name().empty())
531 {
532 irep_idt base_name="#anon"+std::to_string(anon_counter++);
533 p.set_base_name(base_name);
534 }
535
536 // produce identifier
537 irep_idt base_name = p.get_base_name();
538 irep_idt identifier=id2string(symbol.name)+"::"+id2string(base_name);
539
540 p.set_identifier(identifier);
541
542 parameter_symbolt p_symbol;
543
544 p_symbol.type = p.type();
545 p_symbol.name=identifier;
546 p_symbol.base_name=base_name;
547 p_symbol.location = p.source_location();
548
549 symbolt *new_p_symbol;
550 move_symbol(p_symbol, new_p_symbol);
551 }
552
553 // typecheck the body code
555
556 // check the labels
557 for(const auto &label : labels_used)
558 {
559 if(labels_defined.find(label.first) == labels_defined.end())
560 {
561 error().source_location = label.second;
562 error() << "branching label '" << label.first
563 << "' is not defined in function" << eom;
564 throw 0;
565 }
566 }
567}
568
570 const irep_idt &asm_label,
571 symbolt &symbol)
572{
573 const irep_idt orig_name=symbol.name;
574
575 // restrict renaming to functions and global variables;
576 // procedure-local ones would require fixing the scope, as we
577 // do for parameters below
578 if(!asm_label.empty() &&
579 !symbol.is_type &&
580 (symbol.type.id()==ID_code || symbol.is_static_lifetime))
581 {
582 symbol.name=asm_label;
583 symbol.base_name=asm_label;
584 }
585
586 if(symbol.name!=orig_name)
587 {
588 if(!asm_label_map.insert(
589 std::make_pair(orig_name, asm_label)).second)
590 {
591 if(asm_label_map[orig_name]!=asm_label)
592 {
594 error() << "error: replacing asm renaming "
595 << asm_label_map[orig_name] << " by "
596 << asm_label << eom;
597 throw 0;
598 }
599 }
600 }
601 else if(asm_label.empty())
602 {
603 asm_label_mapt::const_iterator entry=
604 asm_label_map.find(symbol.name);
605 if(entry!=asm_label_map.end())
606 {
607 symbol.name=entry->second;
608 symbol.base_name=entry->second;
609 }
610 }
611
612 if(symbol.name!=orig_name &&
613 symbol.type.id()==ID_code &&
614 symbol.value.is_not_nil() && !symbol.is_macro)
615 {
616 const code_typet &code_type=to_code_type(symbol.type);
617
618 for(const auto &p : code_type.parameters())
619 {
620 const irep_idt &p_bn = p.get_base_name();
621 if(p_bn.empty())
622 continue;
623
624 irep_idt p_id=id2string(orig_name)+"::"+id2string(p_bn);
625 irep_idt p_new_id=id2string(symbol.name)+"::"+id2string(p_bn);
626
627 if(!asm_label_map.insert(
628 std::make_pair(p_id, p_new_id)).second)
629 assert(asm_label_map[p_id]==p_new_id);
630 }
631 }
632}
633
635 ansi_c_declarationt &declaration)
636{
637 if(declaration.get_is_static_assert())
638 {
639 codet code(ID_static_assert);
640 code.add_source_location() = declaration.source_location();
641 code.operands().swap(declaration.operands());
642 typecheck_code(code);
643 }
644 else
645 {
646 // get storage spec
647 c_storage_spect c_storage_spec(declaration.type());
648
649 // first typecheck the type of the declaration
650 typecheck_type(declaration.type());
651
652 // mark as 'already typechecked'
654
655 // Now do declarators, if any.
656 for(auto &declarator : declaration.declarators())
657 {
658 c_storage_spect full_spec(declaration.full_type(declarator));
659 full_spec|=c_storage_spec;
660
661 declaration.set_is_inline(full_spec.is_inline);
662 declaration.set_is_static(full_spec.is_static);
663 declaration.set_is_extern(full_spec.is_extern);
664 declaration.set_is_thread_local(full_spec.is_thread_local);
665 declaration.set_is_register(full_spec.is_register);
666 declaration.set_is_typedef(full_spec.is_typedef);
667 declaration.set_is_weak(full_spec.is_weak);
668 declaration.set_is_used(full_spec.is_used);
669
670 symbolt symbol;
671 declaration.to_symbol(declarator, symbol);
672 current_symbol=symbol;
673
674 // now check other half of type
675 typecheck_type(symbol.type);
676
677 if(!full_spec.alias.empty())
678 {
679 if(symbol.value.is_not_nil())
680 {
682 error() << "alias attribute cannot be used with a body"
683 << eom;
684 throw 0;
685 }
686
687 // alias function need not have been declared yet, thus
688 // can't lookup
689 // also cater for renaming/placement in sections
690 const auto &renaming_entry = asm_label_map.find(full_spec.alias);
691 if(renaming_entry == asm_label_map.end())
692 symbol.value = symbol_exprt::typeless(full_spec.alias);
693 else
694 symbol.value = symbol_exprt::typeless(renaming_entry->second);
695 symbol.is_macro=true;
696 }
697
698 if(full_spec.section.empty())
699 apply_asm_label(full_spec.asm_label, symbol);
700 else
701 {
702 // section name is not empty, do a bit of parsing
703 std::string asm_name = id2string(full_spec.section);
704
705 if(asm_name[0] == '.')
706 {
707 std::string::size_type primary_section = asm_name.find('.', 1);
708
709 if(primary_section != std::string::npos)
710 asm_name.resize(primary_section);
711 }
712
713 asm_name += "$$";
714
715 if(!full_spec.asm_label.empty())
716 asm_name+=id2string(full_spec.asm_label);
717 else
718 asm_name+=id2string(symbol.name);
719
720 apply_asm_label(asm_name, symbol);
721 }
722
723 irep_idt identifier=symbol.name;
724 declarator.set_name(identifier);
725
726 typecheck_symbol(symbol);
727
728 // check the contract, if any
729 symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
730 if(new_symbol.type.id() == ID_code)
731 {
732 // We typecheck this after the
733 // function body done above, so as to have parameter symbols
734 // available
735 auto &code_type = to_code_with_contract_type(new_symbol.type);
736
737 for(auto &requires : code_type.requires())
738 {
739 typecheck_expr(requires);
740 implicit_typecast_bool(requires);
742 requires,
743 ID_old,
744 CPROVER_PREFIX "old is not allowed in preconditions.");
746 requires,
747 ID_loop_entry,
748 CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
749 }
750
751 typecheck_spec_assigns(code_type.assigns());
752
753 if(!as_const(code_type).ensures().empty())
754 {
755 const auto &return_type = code_type.return_type();
756
757 if(return_type.id() != ID_empty)
758 parameter_map[CPROVER_PREFIX "return_value"] = return_type;
759
760 for(auto &ensures : code_type.ensures())
761 {
762 typecheck_expr(ensures);
763 implicit_typecast_bool(ensures);
765 ensures,
766 ID_loop_entry,
767 CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
768 }
769
770 if(return_type.id() != ID_empty)
771 parameter_map.erase(CPROVER_PREFIX "return_value");
772 }
773 }
774 }
775 }
776}
ANSI-CC Language Type Checking.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
ANSI-C Language Type Checking.
unsignedbv_typet size_type()
Definition: c_types.cpp:68
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition: c_types.h:418
static void make_already_typechecked(typet &type)
void set_is_thread_local(bool is_thread_local)
void set_is_weak(bool is_weak)
const declaratorst & declarators() const
void set_is_register(bool is_register)
void set_is_inline(bool is_inline)
typet full_type(const ansi_c_declaratort &) const
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
void set_is_extern(bool is_extern)
void set_is_used(bool is_used)
void set_is_typedef(bool is_typedef)
bool get_is_static_assert() const
void set_is_static(bool is_static)
irep_idt asm_label
void typecheck_function_body(symbolt &symbol)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
const irep_idt mode
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
symbol_tablet & symbol_table
virtual std::string to_string(const exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
void typecheck_new_symbol(symbolt &symbol)
asm_label_mapt asm_label_map
virtual void adjust_function_parameter(typet &type) const
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
const irep_idt module
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
virtual void typecheck_spec_assigns(exprt::operandst &targets)
id_type_mapt parameter_map
virtual void implicit_typecast_bool(exprt &expr)
virtual void typecheck_type(typet &type)
void typecheck_symbol(symbolt &symbol)
std::map< irep_idt, source_locationt > labels_defined
Base type of functions.
Definition: std_types.h:539
void set_inlined(bool value)
Definition: std_types.h:670
bool get_inlined() const
Definition: std_types.h:665
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
bool has_ellipsis() const
Definition: std_types.h:611
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
bool is_not_nil() const
Definition: irep.h:380
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:99
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_extern
Definition: symbol.h:66
bool is_macro
Definition: symbol.h:61
bool is_file_local
Definition: symbol.h:66
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
bool is_parameter
Definition: symbol.h:67
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
bool is_weak
Definition: symbol.h:67
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4011
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4027
Deprecated expression utility functions.
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const codet & to_code(const exprt &expr)
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
flavourt mode
Definition: config.h:222