14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_FRESH_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_FRESH_H
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
Rewrites calls to is_fresh predicates into calls to the library implementation.
message_handlert & message_handler
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info)
Rewrites calls to is_fresh predicates into calls to the library implementation in the given program,...
dfcc_is_fresht(dfcc_libraryt &library, message_handlert &message_handler)
Class interface to library types and functions defined in cprover_contracts.c.
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'.