cprover
Loading...
Searching...
No Matches
remove_virtual_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove Virtual Function (Method) Calls
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
12
13#include <algorithm>
14
15#include <util/expr_iterator.h>
16#include <util/expr_util.h>
17#include <util/fresh_symbol.h>
18#include <util/pointer_expr.h>
19#include <util/prefix.h>
20#include <util/symbol_table.h>
21
22#include "class_hierarchy.h"
23#include "class_identifier.h"
24#include "goto_model.h"
25#include "remove_skip.h"
27
62
91
99 const namespacet &ns)
100{
101 call.function() = function_symbol;
102 // Cast the pointers to the correct type for the new callee:
103 // Note the `this` pointer is expected to change type, but other pointers
104 // could also change due to e.g. using a different alias to refer to the same
105 // type (in Java, for example, we see ArrayList.add(ArrayList::E arg)
106 // overriding Collection.add(Collection::E arg))
107 const auto &callee_parameters =
108 to_code_type(ns.lookup(function_symbol.get_identifier()).type).parameters();
109 auto &call_args = call.arguments();
110
111 INVARIANT(
112 callee_parameters.size() == call_args.size(),
113 "function overrides must have matching argument counts");
114
115 for(std::size_t i = 0; i < call_args.size(); ++i)
116 {
117 const typet &need_type = callee_parameters[i].type();
118
119 if(call_args[i].type() != need_type)
120 {
121 // If this wasn't language agnostic code we'd also like to check
122 // compatibility-- for example, Java overrides may have differing generic
123 // qualifiers, but not different base types.
124 INVARIANT(
125 call_args[i].type().id() == ID_pointer,
126 "where overriding function argument types differ, "
127 "those arguments must be pointer-typed");
129 }
130 }
131}
132
146 const goto_programt &goto_program,
150{
152
153 while(instr_it != goto_program.instructions.cbegin())
154 {
155 instr_it = std::prev(instr_it);
156
157 if(instr_it->is_assert())
158 {
159 continue;
160 }
161
162 if(!instr_it->is_assume())
163 {
164 break;
165 }
166
167 exprt guard = instr_it->get_condition();
168
169 bool changed = false;
170 for(auto expr_it = guard.depth_begin(); expr_it != guard.depth_end();
171 ++expr_it)
172 {
174 {
175 expr_it.mutate() = temp_var_for_this;
176 changed = true;
177 }
178 }
179
180 if(changed)
181 {
183 checks_directly_preceding_function_call.instructions.cbegin(),
185 }
186 }
187
189}
190
203 const irep_idt &function_id,
204 const goto_programt &goto_program,
205 const goto_programt::targett target,
207 symbol_table_baset &symbol_table,
210{
212 {
213 // Create a temporary for the `this` argument. This is so that
214 // \ref goto_symext::try_filter_value_sets can reduce the value-set for
215 // `this` to those elements with the correct class identifier.
217 argument_for_this.type(),
218 id2string(function_id),
219 "this_argument",
221 symbol_table.lookup_ref(function_id).mode,
222 symbol_table);
223 const symbol_exprt temp_var_for_this = temp_symbol.symbol_expr();
224
230
233 goto_program, target, argument_for_this, temp_var_for_this);
234
235 new_code_for_this_argument.destructive_append(
237
239 }
240}
241
261 symbol_table_baset &symbol_table,
262 const irep_idt &function_id,
263 goto_programt &goto_program,
265 const dispatch_table_entriest &functions,
267{
268 INVARIANT(
269 target->is_function_call(),
270 "remove_virtual_function must target a FUNCTION_CALL instruction");
271
272 namespacet ns(symbol_table);
273 goto_programt::targett next_target = std::next(target);
274
275 if(functions.empty())
276 {
277 target->turn_into_skip();
278 remove_skip(goto_program, target, next_target);
279 return next_target; // give up
280 }
281
282 // only one option?
283 if(functions.size()==1 &&
285 {
286 if(!functions.front().symbol_expr.has_value())
287 {
288 target->turn_into_skip();
289 remove_skip(goto_program, target, next_target);
290 }
291 else
292 {
293 auto c = code_function_callt(
294 target->call_lhs(), target->call_function(), target->call_arguments());
295 create_static_function_call(c, *functions.front().symbol_expr, ns);
296 target->call_function() = c.function();
297 target->call_arguments() = c.arguments();
298 }
299 return next_target;
300 }
301
302 const auto &vcall_source_loc = target->source_location();
303
305 target->call_lhs(), target->call_function(), target->call_arguments());
307
309 function_id,
310 goto_program,
311 target,
312 code.arguments()[0],
313 symbol_table,
316
317 const exprt &this_expr = code.arguments()[0];
318
319 // Create a skip as the final target for each branch to jump to at the end
321
324
325 // build the calls and gotos
326
329
330 INVARIANT(
331 this_expr.type().id() == ID_pointer, "this parameter must be a pointer");
332 INVARIANT(
333 to_pointer_type(this_expr.type()).base_type() != empty_typet(),
334 "this parameter must not be a void pointer");
335
336 // So long as `this` is already not `void*` typed, the second parameter
337 // is ignored:
340
341 // If instructed, add an ASSUME(FALSE) to handle the case where we don't
342 // match any expected type:
344 {
345 new_code_calls.add(
347 }
348
349 // get initial identifier for grouping
350 INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
351 const auto &last_function_symbol = functions.back().symbol_expr;
352
353 std::map<irep_idt, goto_programt::targett> calls;
354 // Note backwards iteration, to get the fallback candidate first.
355 for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
356 {
357 const auto &fun=*it;
358 irep_idt id_or_empty = fun.symbol_expr.has_value()
359 ? fun.symbol_expr->get_identifier()
360 : irep_idt();
362
363 // Only create one call sequence per possible target:
364 if(insertit.second)
365 {
366 if(fun.symbol_expr.has_value())
367 {
368 // call function
369 auto new_call = code;
370
371 create_static_function_call(new_call, *fun.symbol_expr, ns);
372
375
376 insertit.first->second = t1;
377 }
378 else
379 {
382
383 // No definition for this type; shouldn't be possible...
384 t1->source_location_nonconst().set_comment(
385 "cannot find calls for " +
386 id2string(code.function().get(ID_identifier)) + " dispatching " +
387 id2string(fun.class_id));
388
389 insertit.first->second = t1;
390 }
391
392 // goto final
393 new_code_calls.add(
395 }
396
397 // Fall through to the default callee if possible:
398 if(
401 fun.symbol_expr.has_value() == last_function_symbol.has_value() &&
402 (!fun.symbol_expr.has_value() ||
403 *fun.symbol_expr == *last_function_symbol))
404 {
405 // Nothing to do
406 }
407 else
408 {
412
413 // If the previous GOTO goes to the same callee, join it
414 // (e.g. turning IF x GOTO y into IF x || z GOTO y)
415 if(
416 it != functions.crbegin() &&
417 std::prev(it)->symbol_expr.has_value() == fun.symbol_expr.has_value() &&
418 (!fun.symbol_expr.has_value() ||
419 *(std::prev(it)->symbol_expr) == *fun.symbol_expr))
420 {
421 INVARIANT(
422 !new_code_gotos.empty(),
423 "a dispatch table entry has been processed already, "
424 "which should have created a GOTO");
425 new_code_gotos.instructions.back().condition_nonconst() = or_exprt(
426 new_code_gotos.instructions.back().condition(), class_id_test);
427 }
428 else
429 {
431 insertit.first->second, class_id_test, vcall_source_loc));
432 }
433 }
434 }
435
436 goto_programt new_code;
437
438 // patch them all together
443
444 // set locations
445 for(auto &instruction : new_code.instructions)
446 {
447 source_locationt &source_location = instruction.source_location_nonconst();
448
449 const irep_idt property_class = source_location.get_property_class();
450 const irep_idt comment = source_location.get_comment();
451 source_location = target->source_location();
452 if(!property_class.empty())
453 source_location.set_property_class(property_class);
454 if(!comment.empty())
455 source_location.set_comment(comment);
456 }
457
458 goto_program.destructive_insert(next_target, new_code);
459
460 // finally, kill original invocation
461 target->turn_into_skip();
462
463 // only remove skips within the virtual-function handling block
464 remove_skip(goto_program, target, next_target);
465
466 return next_target;
467}
468
479 const irep_idt &function_id,
480 goto_programt &goto_program,
482{
483 const exprt &function = as_const(*target).call_function();
484 INVARIANT(
486 "remove_virtual_function must take a function call instruction whose "
487 "function is a class method descriptor ");
488 INVARIANT(
489 !as_const(*target).call_arguments().empty(),
490 "virtual function calls must have at least a this-argument");
491
493 dispatch_table_entriest functions;
494 get_callees.get_functions(function, functions);
495
498 function_id,
499 goto_program,
500 target,
501 functions,
503}
504
519 const irep_idt &this_id,
521 const irep_idt &component_name,
522 dispatch_table_entriest &functions,
523 dispatch_table_entries_mapt &entry_map) const
524{
527 return;
528
529 for(const auto &child : findit->second.children)
530 {
531 // Skip if we have already visited this and we found a function call that
532 // did not resolve to non java.lang.Object.
533 auto it = entry_map.find(child);
534 if(
535 it != entry_map.end() &&
536 (!it->second.symbol_expr.has_value() ||
537 !has_prefix(
538 id2string(it->second.symbol_expr->get_identifier()),
539 "java::java.lang.Object")))
540 {
541 continue;
542 }
543 exprt method = get_method(child, component_name);
545 if(method.is_not_nil())
546 {
547 function.symbol_expr=to_symbol_expr(method);
548 function.symbol_expr->set(ID_C_class, child);
549 }
550 else
551 {
553 }
554 if(!function.symbol_expr.has_value())
555 {
557 component_name, child, symbol_table);
558 if(resolved_call)
559 {
560 function.class_id = resolved_call->get_class_identifier();
562 resolved_call->get_full_component_identifier());
563
564 function.symbol_expr = called_symbol.symbol_expr();
565 function.symbol_expr->set(
566 ID_C_class, resolved_call->get_class_identifier());
567 }
568 }
569 functions.push_back(function);
570 entry_map.emplace(child, function);
571
573 child, function.symbol_expr, component_name, functions, entry_map);
574 }
575}
576
582 const exprt &function,
583 dispatch_table_entriest &functions) const
584{
585 // class part of function to call
586 const irep_idt class_id=function.get(ID_C_class);
587 const std::string class_id_string(id2string(class_id));
588 const irep_idt function_name = function.get(ID_component_name);
589 const std::string function_name_string(id2string(function_name));
590 INVARIANT(!class_id.empty(), "All virtual functions must have a class");
591
592 auto resolved_call =
593 get_inherited_method_implementation(function_name, class_id, symbol_table);
594
595 // might be an abstract function
597
598 if(resolved_call)
599 {
600 root_function.class_id = resolved_call->get_class_identifier();
601
602 const symbolt &called_symbol =
603 symbol_table.lookup_ref(resolved_call->get_full_component_identifier());
604
605 root_function.symbol_expr=called_symbol.symbol_expr();
606 root_function.symbol_expr->set(
607 ID_C_class, resolved_call->get_class_identifier());
608 }
609
610 // iterate over all children, transitively
613 class_id, root_function.symbol_expr, function_name, functions, entry_map);
614
615 if(root_function.symbol_expr.has_value())
616 functions.push_back(root_function);
617
618 // Sort for the identifier of the function call symbol expression, grouping
619 // together calls to the same function. Keep java.lang.Object entries at the
620 // end for fall through. The reasoning is that this is the case with most
621 // entries in realistic cases.
622 std::sort(
623 functions.begin(),
624 functions.end(),
626 irep_idt a_id = a.symbol_expr.has_value()
627 ? a.symbol_expr->get_identifier()
628 : irep_idt();
629 irep_idt b_id = b.symbol_expr.has_value()
630 ? b.symbol_expr->get_identifier()
631 : irep_idt();
632
633 if(has_prefix(id2string(a_id), "java::java.lang.Object"))
634 return false;
635 else if(has_prefix(id2string(b_id), "java::java.lang.Object"))
636 return true;
637 else
638 {
639 int cmp = a_id.compare(b_id);
640 if(cmp == 0)
641 return a.class_id < b.class_id;
642 else
643 return cmp < 0;
644 }
645 });
646}
647
654 const irep_idt &class_id,
655 const irep_idt &component_name) const
656{
657 const irep_idt &id=
659 class_id, component_name);
660
661 const symbolt *symbol;
662 if(ns.lookup(id, symbol))
663 return nil_exprt();
664
665 return symbol->symbol_expr();
666}
667
672 const irep_idt &function_id,
673 goto_programt &goto_program)
674{
675 bool did_something=false;
676
677 for(goto_programt::instructionst::iterator
678 target = goto_program.instructions.begin();
679 target != goto_program.instructions.end();
680 ) // remove_virtual_function returns the next instruction to process
681 {
682 if(target->is_function_call())
683 {
685 as_const(*target).call_function()))
686 {
687 target = remove_virtual_function(function_id, goto_program, target);
688 did_something=true;
689 continue;
690 }
691 }
692
693 ++target;
694 }
695
696 if(did_something)
697 goto_program.update();
698
699 return did_something;
700}
701
705{
706 bool did_something=false;
707
708 for(goto_functionst::function_mapt::iterator f_it=
709 functions.function_map.begin();
710 f_it!=functions.function_map.end();
711 f_it++)
712 {
713 const irep_idt &function_id = f_it->first;
714 goto_programt &goto_program=f_it->second.body;
715
716 if(remove_virtual_functions(function_id, goto_program))
717 did_something=true;
718 }
719
720 if(did_something)
721 functions.compute_location_numbers();
722}
723
729 symbol_table_baset &symbol_table,
730 goto_functionst &goto_functions)
731{
732 class_hierarchyt class_hierarchy;
733 class_hierarchy(symbol_table);
734 remove_virtual_functionst rvf(symbol_table, class_hierarchy);
735 rvf(goto_functions);
736}
737
746 symbol_table_baset &symbol_table,
747 goto_functionst &goto_functions,
748 const class_hierarchyt &class_hierarchy)
749{
750 remove_virtual_functionst rvf(symbol_table, class_hierarchy);
751 rvf(goto_functions);
752}
753
757{
759 goto_model.symbol_table, goto_model.goto_functions);
760}
761
768 goto_modelt &goto_model,
769 const class_hierarchyt &class_hierarchy)
770{
772 goto_model.symbol_table, goto_model.goto_functions, class_hierarchy);
773}
774
780{
781 class_hierarchyt class_hierarchy;
782 class_hierarchy(function.get_symbol_table());
783 remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
784 rvf.remove_virtual_functions(
785 function.get_function_id(), function.get_goto_function().body);
786}
787
796 goto_model_functiont &function,
797 const class_hierarchyt &class_hierarchy)
798{
799 remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
800 rvf.remove_virtual_functions(
801 function.get_function_id(), function.get_goto_function().body);
802}
803
823 symbol_tablet &symbol_table,
824 const irep_idt &function_id,
825 goto_programt &goto_program,
826 goto_programt::targett instruction,
829{
831 symbol_table,
832 function_id,
833 goto_program,
834 instruction,
837
838 goto_program.update();
839
840 return next;
841}
842
844 goto_modelt &goto_model,
845 const irep_idt &function_id,
846 goto_programt &goto_program,
847 goto_programt::targett instruction,
850{
852 goto_model.symbol_table,
853 function_id,
854 goto_program,
855 instruction,
858}
859
861 const exprt &function,
862 const symbol_table_baset &symbol_table,
863 const class_hierarchyt &class_hierarchy,
865{
866 get_virtual_calleest get_callees(symbol_table, class_hierarchy);
867 get_callees.get_functions(function, overridden_functions);
868}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
std::set< irep_idt > get_callees(const call_grapht::directed_grapht &graph, const irep_idt &function)
Get functions directly callable from a given function.
Class Hierarchy.
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
Extract class identifier.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Non-graph-based representation of the class hierarchy.
codet representation of a function call statement.
const parameterst & parameters() const
Definition std_types.h:655
A constant literal expression.
Definition std_expr.h:2807
optionalt< symbol_exprt > symbol_expr
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
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
depth_iteratort depth_end()
Definition expr.cpp:267
depth_iteratort depth_begin()
Definition expr.cpp:265
typet & type()
Return the type of the expression.
Definition expr.h:82
The Boolean constant false.
Definition std_expr.h:2865
const symbol_table_baset & symbol_table
void get_child_functions_rec(const irep_idt &, const optionalt< symbol_exprt > &, const irep_idt &, dispatch_table_entriest &, dispatch_table_entries_mapt &) const
Used by get_functions to track the most-derived parent that provides an override of a given function.
std::function< optionalt< resolve_inherited_componentt::inherited_componentt >(const irep_idt &, const irep_idt &)> function_call_resolvert
get_virtual_calleest(const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
exprt get_method(const irep_idt &class_id, const irep_idt &component_name) const
Returns symbol pointing to a specified method in a specified class.
void get_functions(const exprt &, dispatch_table_entriest &) const
Used to get dispatch entries to call for the given function.
const class_hierarchyt & class_hierarchy
A collection of goto functions.
function_mapt function_map
void compute_location_numbers()
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:183
const irep_idt & get_function_id()
Get function id.
Definition goto_model.h:232
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition goto_model.h:225
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition goto_model.h:218
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
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.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:2874
Boolean OR.
Definition std_expr.h:2082
const typet & base_type() const
The type of the data what we point to.
remove_virtual_functionst(symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
bool remove_virtual_functions(const irep_idt &function_id, goto_programt &goto_program)
Remove all virtual function calls in a GOTO program and replace them with calls to their most derived...
void operator()(goto_functionst &functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
goto_programt::targett remove_virtual_function(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target)
Replace specified virtual function call with a static call to its most derived implementation.
const class_hierarchyt & class_hierarchy
static irep_idt build_full_component_identifier(const irep_idt &class_name, const irep_idt &component_name)
Build a component name as found in a GOTO symbol table equivalent to the name of a concrete component...
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_property_class() const
const irep_idt & get_comment() const
String type.
Definition std_types.h:901
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
Expression to hold a symbol (variable)
Definition std_expr.h:80
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:2856
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Symbol Table + CFG.
dstringt irep_idt
Definition irep.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
static void process_this_argument(const irep_idt &function_id, const goto_programt &goto_program, const goto_programt::targett target, exprt &argument_for_this, symbol_table_baset &symbol_table, const source_locationt &vcall_source_loc, goto_programt &new_code_for_this_argument)
If argument_for_this contains a dereference then create a temporary variable for it and use that inst...
static goto_programt::targett replace_virtual_function_with_dispatch_table(symbol_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target, const dispatch_table_entriest &functions, virtual_dispatch_fallback_actiont fallback_action)
Replace virtual function call with a static function call Achieved by substituting a virtual function...
static goto_programt analyse_checks_directly_preceding_function_call(const goto_programt &goto_program, goto_programt::const_targett instr_it, const exprt &argument_for_this, const symbol_exprt &temp_var_for_this)
Duplicate ASSUME instructions involving argument_for_this for temp_var_for_this.
static void create_static_function_call(code_function_callt &call, const symbol_exprt &function_symbol, const namespacet &ns)
Create a concrete function call to replace a virtual one.
void collect_virtual_function_callees(const exprt &function, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions)
Given a function expression representing a virtual method of a class, the function computes all overr...
goto_programt::targett remove_virtual_function(symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action)
Replace virtual function call with a static function call Achieved by substituting a virtual function...
void remove_virtual_functions(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Functions for replacing virtual function call with a static function calls in functions,...
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
@ ASSUME_FALSE
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.
@ CALL_LAST_FUNCTION
When no callee type matches, call the last passed function, which is expected to be some safe default...
std::vector< dispatch_table_entryt > dispatch_table_entriest
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_method_implementation(const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table)
Given a class and a component, identify the concrete method it is resolved to.
Given a class and a component (either field or method), find the closest parent that defines that com...
#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
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Author: Diffblue Ltd.