14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_OBEYS_CONTRACT_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_OBEYS_CONTRACT_H
44 std::set<irep_idt> &function_pointer_contracts);
55 std::set<irep_idt> &function_pointer_contracts);
67 std::set<irep_idt> &function_pointer_contracts);
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
Class interface to library types and functions defined in cprover_contracts.c.
Rewrites calls to obeys_contract predicates into calls to the library implementation.
dfcc_obeys_contractt(dfcc_libraryt &library, message_handlert &message_handler)
message_handlert & message_handler
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Rewrites calls to obeys_contract predicates into calls to the library implementation in the given pro...
void get_contract_name(const exprt &expr, std::set< irep_idt > &function_pointer_contracts)
Extracts the name from the second argument of a call to obeys_contract (modulo any intermediate typec...
Base class for all expressions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
Class that provides messages with a built-in verbosity 'level'.