cprover
Loading...
Searching...
No Matches
goto_inline_class.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Function Inlining
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_inline_class.h"
13
14#ifdef DEBUG
15#include <iostream>
16#endif
17
18#include <util/cprover_prefix.h>
19#include <util/invariant.h>
20#include <util/std_code.h>
21#include <util/symbol.h>
22
24 const goto_programt::targett target,
25 const irep_idt &function_name, // name of called function
26 const goto_functiont::parameter_identifierst &parameter_identifiers,
27 const exprt::operandst &arguments, // arguments of call
28 goto_programt &dest)
29{
30 PRECONDITION(target->is_function_call());
31 PRECONDITION(dest.empty());
32
33 const source_locationt &source_location = target->source_location();
34
35 // iterates over the operands
36 exprt::operandst::const_iterator it1=arguments.begin();
37
38 // iterates over the parameters
39 for(const auto &identifier : parameter_identifiers)
40 {
42 !identifier.empty(),
43 source_location.as_string() + ": no identifier for function parameter");
44
45 const symbolt &symbol = ns.lookup(identifier);
46
47 // this is the type the n-th argument should have
48 const typet &parameter_type = symbol.type;
49
51 dest.add(goto_programt::make_decl(symbol.symbol_expr(), source_location));
52 decl->code_nonconst().add_source_location() = source_location;
53
54 // this is the actual parameter
55 exprt actual;
56
57 // if you run out of actual arguments there was a mismatch
58 if(it1==arguments.end())
59 {
60 log.warning().source_location = source_location;
61 log.warning() << "call to '" << function_name << "': "
62 << "not enough arguments, "
63 << "inserting non-deterministic value" << messaget::eom;
64
65 actual = side_effect_expr_nondett(parameter_type, source_location);
66 }
67 else
68 actual=*it1;
69
70 // nil means "don't assign"
71 if(actual.is_nil())
72 {
73 }
74 else
75 {
76 // it should be the same exact type as the parameter,
77 // subject to some exceptions
78 if(parameter_type != actual.type())
79 {
80 const typet &f_partype = parameter_type;
81 const typet &f_acttype = actual.type();
82
83 // we are willing to do some conversion
84 if(
85 (f_partype.id() == ID_pointer && f_acttype.id() == ID_pointer) ||
86 (f_partype.id() == ID_pointer && f_acttype.id() == ID_array &&
87 to_type_with_subtype(f_partype).subtype() ==
88 to_type_with_subtype(f_acttype).subtype()))
89 {
90 actual = typecast_exprt(actual, f_partype);
91 }
92 else if((f_partype.id()==ID_signedbv ||
93 f_partype.id()==ID_unsignedbv ||
94 f_partype.id()==ID_bool) &&
95 (f_acttype.id()==ID_signedbv ||
96 f_acttype.id()==ID_unsignedbv ||
97 f_acttype.id()==ID_bool))
98 {
99 actual = typecast_exprt(actual, f_partype);
100 }
101 else
102 {
104 }
105 }
106
107 // adds an assignment of the actual parameter to the formal parameter
108 code_assignt assignment(symbol_exprt(identifier, parameter_type), actual);
109 assignment.add_source_location()=source_location;
110
111 dest.add(goto_programt::make_assignment(assignment, source_location));
112 }
113
114 if(it1!=arguments.end())
115 ++it1;
116 }
117
118 if(it1!=arguments.end())
119 {
120 // too many arguments -- we just ignore that, no harm done
121 }
122}
123
125 const goto_programt::targett target,
126 const goto_functiont::parameter_identifierst &parameter_identifiers,
127 goto_programt &dest)
128{
129 PRECONDITION(target->is_function_call());
130 PRECONDITION(dest.empty());
131
132 const source_locationt &source_location = target->source_location();
133
134 for(const auto &identifier : parameter_identifiers)
135 {
136 INVARIANT(
137 !identifier.empty(),
138 source_location.as_string() + ": no identifier for function parameter");
139
140 {
141 const symbolt &symbol=ns.lookup(identifier);
142
143 goto_programt::targett dead = dest.add(
144 goto_programt::make_dead(symbol.symbol_expr(), source_location));
145 dead->code_nonconst().add_source_location() = source_location;
146 }
147 }
148}
149
151 goto_programt &dest, // inlining this
152 const exprt &lhs) // lhs in caller
153{
154 for(goto_programt::instructionst::iterator
155 it=dest.instructions.begin();
156 it!=dest.instructions.end();
157 it++)
158 {
159 if(it->is_set_return_value())
160 {
161 if(lhs.is_not_nil())
162 {
163 // a typecast may be necessary if the declared return type at the call
164 // site differs from the defined return type
166 lhs,
167 typecast_exprt::conditional_cast(it->return_value(), lhs.type()),
168 it->source_location());
169 }
170 else
171 {
173 code_expressiont(it->return_value()), it->source_location());
174 }
175 }
176 }
177}
178
180 source_locationt &dest,
181 const source_locationt &new_location)
182{
183 // we copy, and then adjust for property_id, property_class
184 // and comment, if necessary
185
187 irep_idt property_class=dest.get_property_class();
188 irep_idt property_id=dest.get_property_id();
189
190 dest=new_location;
191
192 if(!comment.empty())
193 dest.set_comment(comment);
194
195 if(!property_class.empty())
196 dest.set_property_class(property_class);
197
198 if(!property_id.empty())
199 dest.set_property_id(property_id);
200}
201
203 exprt &dest,
204 const source_locationt &new_location)
205{
206 Forall_operands(it, dest)
207 replace_location(*it, new_location);
208
209 if(dest.find(ID_C_source_location).is_not_nil())
210 replace_location(dest.add_source_location(), new_location);
211}
212
214 const goto_functiont &goto_function,
215 goto_programt &dest,
217 const exprt &lhs,
218 const symbol_exprt &function,
219 const exprt::operandst &arguments)
220{
221 PRECONDITION(target->is_function_call());
222 PRECONDITION(!dest.empty());
223 PRECONDITION(goto_function.body_available());
224
225 const irep_idt identifier=function.get_identifier();
226
227 goto_programt body;
228 body.copy_from(goto_function.body);
229 inline_log.copy_from(goto_function.body, body);
230
233 end.is_end_function(),
234 "final instruction of a function must be an END_FUNCTION");
236
237 // make sure the inlined function does not introduce hiding
238 if(goto_function.is_hidden())
239 {
240 for(auto &instruction : body.instructions)
241 instruction.labels.remove(CPROVER_PREFIX "HIDE");
242 }
243
244 replace_return(body, lhs);
245
246 goto_programt tmp1;
248 target, identifier, goto_function.parameter_identifiers, arguments, tmp1);
249
250 goto_programt tmp2;
251 parameter_destruction(target, goto_function.parameter_identifiers, tmp2);
252
253 goto_programt tmp;
254 tmp.destructive_append(tmp1); // par assignment
255 tmp.destructive_append(body); // body
256 tmp.destructive_append(tmp2); // par destruction
257
259 t_it=goto_function.body.instructions.begin();
260 unsigned begin_location_number=t_it->location_number;
261 t_it=--goto_function.body.instructions.end();
263 t_it->is_end_function(),
264 "final instruction of a function must be an END_FUNCTION");
265 unsigned end_location_number=t_it->location_number;
266
267 unsigned call_location_number=target->location_number;
268
270 tmp,
271 begin_location_number,
272 end_location_number,
273 call_location_number,
274 identifier);
275
277 {
278 for(auto &instruction : tmp.instructions)
279 {
281 instruction.source_location_nonconst(), target->source_location());
282 replace_location(instruction.code_nonconst(), target->source_location());
283
284 if(instruction.has_condition())
285 {
287 instruction.condition_nonconst(), target->source_location());
288 }
289 }
290 }
291
292 // kill call
293 *target = goto_programt::make_location(target->source_location());
294 target++;
295
296 dest.destructive_insert(target, tmp);
297}
298
302 goto_programt &dest,
303 const inline_mapt &inline_map,
304 const bool transitive,
305 const bool force_full,
307{
308 PRECONDITION(target->is_function_call());
309 PRECONDITION(!dest.empty());
310 PRECONDITION(!transitive || inline_map.empty());
311
312#ifdef DEBUG
313 std::cout << "Expanding call:\n";
314 dest.output_instruction(ns, irep_idt(), std::cout, *target);
315#endif
316
317 exprt lhs;
318 exprt function_expr;
319 exprt::operandst arguments;
320
321 get_call(target, lhs, function_expr, arguments);
322
323 if(function_expr.id()!=ID_symbol)
324 return;
325
326 const symbol_exprt &function=to_symbol_expr(function_expr);
327
328 const irep_idt identifier=function.get_identifier();
329
330 if(is_ignored(identifier))
331 return;
332
333 // see if we are already expanding it
334 if(recursion_set.find(identifier)!=recursion_set.end())
335 {
336 // it's recursive.
337 // Uh. Buh. Give up.
339 log.warning() << "recursion is ignored on call to '" << identifier << "'"
340 << messaget::eom;
341
342 if(force_full)
343 target->turn_into_skip();
344
345 return;
346 }
347
348 goto_functionst::function_mapt::iterator f_it=
349 goto_functions.function_map.find(identifier);
350
351 if(f_it==goto_functions.function_map.end())
352 {
354 log.warning() << "missing function '" << identifier << "' is ignored"
355 << messaget::eom;
356
357 if(force_full)
358 target->turn_into_skip();
359
360 return;
361 }
362
363 // function to inline
364 goto_functiont &goto_function=f_it->second;
365
366 if(goto_function.body_available())
367 {
368 if(transitive)
369 {
370 const goto_functiont &cached=
372 identifier,
373 goto_function,
374 force_full);
375
376 // insert 'cached' into 'dest' at 'target'
378 cached,
379 dest,
380 target,
381 lhs,
382 function,
383 arguments);
384
385 log.progress() << "Inserting " << identifier << " into caller"
386 << messaget::eom;
387 log.progress() << "Number of instructions: "
388 << cached.body.instructions.size() << messaget::eom;
389
390 if(!caching)
391 {
392 log.progress() << "Removing " << identifier << " from cache"
393 << messaget::eom;
394 log.progress() << "Number of instructions: "
395 << cached.body.instructions.size() << messaget::eom;
396
397 inline_log.cleanup(cached.body);
398 cache.erase(identifier);
399 }
400 }
401 else
402 {
403 // inline non-transitively
405 identifier,
406 goto_function,
407 inline_map,
408 force_full);
409
410 // insert 'goto_function' into 'dest' at 'target'
412 goto_function,
413 dest,
414 target,
415 lhs,
416 function,
417 arguments);
418 }
419 }
420 else // no body available
421 {
422 if(no_body_set.insert(identifier).second) // newly inserted
423 {
425 log.warning() << "no body for function '" << identifier << "'"
426 << messaget::eom;
427 }
428 }
429}
430
433 exprt &lhs,
434 exprt &function,
435 exprt::operandst &arguments)
436{
437 PRECONDITION(it->is_function_call());
438
439 lhs = it->call_lhs();
440 function = it->call_function();
441 arguments = it->call_arguments();
442}
443
450 const inline_mapt &inline_map,
451 const bool force_full)
452{
453 PRECONDITION(check_inline_map(inline_map));
454
455 for(auto &gf_entry : goto_functions.function_map)
456 {
457 const irep_idt identifier = gf_entry.first;
458 DATA_INVARIANT(!identifier.empty(), "function name must not be empty");
459 goto_functiont &goto_function = gf_entry.second;
460
461 if(!goto_function.body_available())
462 continue;
463
464 goto_inline(identifier, goto_function, inline_map, force_full);
465 }
466}
467
476 const irep_idt identifier,
477 goto_functiont &goto_function,
478 const inline_mapt &inline_map,
479 const bool force_full)
480{
481 recursion_set.clear();
482
484 identifier,
485 goto_function,
486 inline_map,
487 force_full);
488}
489
491 const irep_idt identifier,
492 goto_functiont &goto_function,
493 const inline_mapt &inline_map,
494 const bool force_full)
495{
496 PRECONDITION(goto_function.body_available());
497
498 finished_sett::const_iterator f_it=finished_set.find(identifier);
499
500 if(f_it!=finished_set.end())
501 return;
502
503 PRECONDITION(check_inline_map(identifier, inline_map));
504
505 goto_programt &goto_program=goto_function.body;
506
507 const inline_mapt::const_iterator im_it=inline_map.find(identifier);
508
509 if(im_it==inline_map.end())
510 return;
511
512 const call_listt &call_list=im_it->second;
513
514 if(call_list.empty())
515 return;
516
517 recursion_set.insert(identifier);
518
519 for(const auto &call : call_list)
520 {
521 const bool transitive=call.second;
522
523 const inline_mapt &new_inline_map=
524 transitive?inline_mapt():inline_map;
525
527 goto_program,
528 new_inline_map,
529 transitive,
530 force_full,
531 call.first);
532 }
533
534 recursion_set.erase(identifier);
535
536 // remove_skip(goto_program);
537 // goto_program.update(); // does not change loop ids
538
539 finished_set.insert(identifier);
540}
541
543 const irep_idt identifier,
544 const goto_functiont &goto_function,
545 const bool force_full)
546{
547 PRECONDITION(goto_function.body_available());
548
549 cachet::const_iterator c_it=cache.find(identifier);
550
551 if(c_it!=cache.end())
552 {
553 const goto_functiont &cached=c_it->second;
555 cached.body_available(),
556 "body of cached functions must be available");
557 return cached;
558 }
559
560 goto_functiont &cached=cache[identifier];
562 cached.body.empty(), "body of new function in cache must be empty");
563
564 log.progress() << "Creating copy of " << identifier << messaget::eom;
565 log.progress() << "Number of instructions: "
566 << goto_function.body.instructions.size() << messaget::eom;
567
568 cached.copy_from(goto_function); // location numbers not changed
569 inline_log.copy_from(goto_function.body, cached.body);
570
571 goto_programt &goto_program=cached.body;
572
573 goto_programt::targetst call_list;
574
575 Forall_goto_program_instructions(i_it, goto_program)
576 {
577 if(i_it->is_function_call())
578 call_list.push_back(i_it);
579 }
580
581 if(call_list.empty())
582 return cached;
583
584 recursion_set.insert(identifier);
585
586 for(const auto &call : call_list)
587 {
589 goto_program,
590 inline_mapt(),
591 true,
592 force_full,
593 call);
594 }
595
596 recursion_set.erase(identifier);
597
598 // remove_skip(goto_program);
599 // goto_program.update(); // does not change loop ids
600
601 return cached;
602}
603
605{
606 return id == CPROVER_PREFIX "cleanup" || id == CPROVER_PREFIX "set_must" ||
607 id == CPROVER_PREFIX "set_may" || id == CPROVER_PREFIX "clear_must" ||
608 id == CPROVER_PREFIX "clear_may" || id == CPROVER_PREFIX "cover";
609}
610
612 const irep_idt identifier,
613 const inline_mapt &inline_map) const
614{
615 goto_functionst::function_mapt::const_iterator f_it=
616 goto_functions.function_map.find(identifier);
617
619
620 inline_mapt::const_iterator im_it=inline_map.find(identifier);
621
622 if(im_it==inline_map.end())
623 return true;
624
625 const call_listt &call_list=im_it->second;
626
627 if(call_list.empty())
628 return true;
629
631
632 for(const auto &call : call_list)
633 {
634 const goto_programt::const_targett target=call.first;
635
636 #if 0
637 // might not hold if call was previously inlined
638 if(target->function!=identifier)
639 return false;
640 #endif
641
642 // location numbers increasing
643 if(
645 target->location_number <= ln)
646 {
647 return false;
648 }
649
650 if(!target->is_function_call())
651 return false;
652
653 ln=target->location_number;
654 }
655
656 return true;
657}
658
659bool goto_inlinet::check_inline_map(const inline_mapt &inline_map) const
660{
661 for(const auto &gf_entry : goto_functions.function_map)
662 {
663 if(!check_inline_map(gf_entry.first, inline_map))
664 return false;
665 }
666
667 return true;
668}
669
671 std::ostream &out,
672 const inline_mapt &inline_map)
673{
674 PRECONDITION(check_inline_map(inline_map));
675
676 for(const auto &it : inline_map)
677 {
678 const irep_idt &id=it.first;
679 const call_listt &call_list=it.second;
680
681 out << "Function: " << id << "\n";
682
683 goto_functionst::function_mapt::const_iterator f_it=
685
686 if(f_it!=goto_functions.function_map.end() &&
687 !call_list.empty())
688 {
689 const goto_functiont &goto_function=f_it->second;
691 goto_function.body_available(),
692 "cannot inline function with empty body");
693
694 const goto_programt &goto_program=goto_function.body;
695
696 for(const auto &call : call_list)
697 {
698 const goto_programt::const_targett target=call.first;
699 bool transitive=call.second;
700
701 out << " Call:\n";
702 goto_program.output_instruction(ns, id, out, *target);
703 out << " Transitive: " << transitive << "\n";
704 }
705 }
706 else
707 {
708 out << " -\n";
709 }
710 }
711}
712
713void goto_inlinet::output_cache(std::ostream &out) const
714{
715 for(auto it=cache.begin(); it!=cache.end(); it++)
716 {
717 if(it!=cache.begin())
718 out << ", ";
719
720 out << it->first << "\n";
721 }
722}
723
724// remove segment that refer to the given goto program
726 const goto_programt &goto_program)
727{
728 forall_goto_program_instructions(it, goto_program)
729 log_map.erase(it);
730}
731
733 const goto_functionst::function_mapt &function_map)
734{
735 for(const auto &it : function_map)
736 {
737 const goto_functiont &goto_function=it.second;
738
739 if(!goto_function.body_available())
740 continue;
741
742 cleanup(goto_function.body);
743 }
744}
745
747 const goto_programt &goto_program,
748 const unsigned begin_location_number,
749 const unsigned end_location_number,
750 const unsigned call_location_number,
751 const irep_idt function)
752{
753 PRECONDITION(!goto_program.empty());
754 PRECONDITION(!function.empty());
755 PRECONDITION(end_location_number >= begin_location_number);
756
757 goto_programt::const_targett start=goto_program.instructions.begin();
758 INVARIANT(
759 log_map.find(start) == log_map.end(),
760 "inline function should be registered once in map of inline functions");
761
762 goto_programt::const_targett end=goto_program.instructions.end();
763 end--;
764
766 info.begin_location_number=begin_location_number;
767 info.end_location_number=end_location_number;
768 info.call_location_number=call_location_number;
769 info.function=function;
770 info.end=end;
771
772 log_map[start]=info;
773}
774
776 const goto_programt &from,
777 const goto_programt &to)
778{
779 PRECONDITION(from.instructions.size() == to.instructions.size());
780
783
784 for(; it1!=from.instructions.end(); it1++, it2++)
785 {
787 it2 != to.instructions.end(),
788 "'to' target function is not allowed to be empty");
790 it1->location_number == it2->location_number,
791 "both functions' instruction should point to the same source");
792
793 log_mapt::const_iterator l_it=log_map.find(it1);
794 if(l_it!=log_map.end()) // a segment starts here
795 {
796 // as 'to' is a fresh copy
798 log_map.find(it2) == log_map.end(),
799 "'to' target is not expected to be in the log_map");
800
801 goto_inline_log_infot info=l_it->second;
803
804 // find end of new
807 while(tmp_it!=end)
808 {
809 new_end++;
810 tmp_it++;
811 }
812
813 info.end=new_end;
814
815 log_map[it2]=info;
816 }
817 }
818}
819
820// call after goto_functions.update()!
822{
823 json_objectt json_result;
824 json_arrayt &json_inlined=json_result["inlined"].make_array();
825
826 for(const auto &it : log_map)
827 {
828 goto_programt::const_targett start=it.first;
829 const goto_inline_log_infot &info=it.second;
831
832 PRECONDITION(start->location_number <= end->location_number);
833
834 json_arrayt json_orig{
835 json_numbert(std::to_string(info.begin_location_number)),
836 json_numbert(std::to_string(info.end_location_number))};
837 json_arrayt json_new{json_numbert(std::to_string(start->location_number)),
838 json_numbert(std::to_string(end->location_number))};
839
840 json_objectt object{
841 {"call", json_numbert(std::to_string(info.call_location_number))},
842 {"function", json_stringt(info.function.c_str())},
843 {"originalSegment", std::move(json_orig)},
844 {"inlinedSegment", std::move(json_new)}};
845
846 json_inlined.push_back(std::move(object));
847 }
848
849 return std::move(json_result);
850}
A codet representing an assignment in the program.
codet representation of an expression statement.
Definition std_code.h:1394
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
const char * c_str() const
Definition dstring.h:99
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
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
source_locationt & add_source_location()
Definition expr.h:235
std::map< irep_idt, goto_functiont > function_mapt
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
bool is_hidden() const
std::vector< irep_idt > parameter_identifierst
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
void copy_from(const goto_functiont &other)
bool body_available() const
void copy_from(const goto_programt &from, const goto_programt &to)
void cleanup(const goto_programt &goto_program)
void add_segment(const goto_programt &goto_program, const unsigned begin_location_number, const unsigned end_location_number, const unsigned call_location_number, const irep_idt function)
bool is_ignored(const irep_idt id) const
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
std::list< callt > call_listt
goto_functionst & goto_functions
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
no_body_sett no_body_set
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
Inline all of the chosen calls in a given function.
recursion_sett recursion_set
void insert_function_body(const goto_functiont &f, goto_programt &dest, goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
bool check_inline_map(const inline_mapt &inline_map) const
void parameter_destruction(const goto_programt::targett target, const goto_functiont::parameter_identifierst &parameter_identifiers, goto_programt &dest)
const bool adjust_function
goto_inline_logt inline_log
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
goto_functionst::goto_functiont goto_functiont
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const goto_functiont::parameter_identifierst &parameter_identifiers, const exprt::operandst &arguments, goto_programt &dest)
std::map< irep_idt, call_listt > inline_mapt
void replace_return(goto_programt &body, const exprt &lhs)
finished_sett finished_set
const namespacet & ns
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
Inlines a single function call Calls out to goto_inline_transitive or goto_inline_nontransitive.
void output_cache(std::ostream &out) const
This class represents an instruction in the GOTO intermediate representation.
static const unsigned nil_target
Uniquely identify an invalid target or location.
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
instructionst::const_iterator const_targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static instructiont make_location(const source_locationt &l)
targett add(instructiont &&instruction)
Adds a given instruction at the end.
bool empty() const
Is the program empty?
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
std::list< targett > targetst
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
jsont & push_back(const jsont &json)
Definition json.h:212
Definition json.h:27
json_arrayt & make_array()
Definition json.h:420
source_locationt source_location
Definition message.h:247
mstreamt & warning() const
Definition message.h:404
mstreamt & progress() const
Definition message.h:424
static eomt eom
Definition message.h:297
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
void set_comment(const irep_idt &comment)
void set_property_id(const irep_idt &property_id)
const irep_idt & get_property_id() const
void set_property_class(const irep_idt &property_class)
const irep_idt & get_property_class() const
std::string as_string() const
const irep_idt & get_comment() const
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
Symbol table entry.
Definition symbol.h:28
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:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
#define CPROVER_PREFIX
#define Forall_operands(it, expr)
Definition expr.h:25
void replace_location(source_locationt &dest, const source_locationt &new_location)
Function Inlining This is a class that encapsulates the state and functionality needed to do inline m...
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
dstringt irep_idt
Definition irep.h:37
static std::string comment(const rw_set_baset::entryt &entry, bool write)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
Symbol table entry.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177