15#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SPEC_FUNCTIONS_H
16#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SPEC_FUNCTIONS_H
87 std::size_t &nof_targets);
113 const exprt &write_set_to_havoc,
116 std::size_t &nof_targets);
141 std::size_t &nof_targets);
163 const exprt &write_set_to_fill,
166 std::size_t &nof_targets);
212 const exprt &write_set_to_fill,
215 std::size_t &nof_targets);
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Class interface to library types and functions defined in cprover_contracts.c.
void to_spec_assigns_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
void to_spec_frees_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying freeable targets declaratively u...
void generate_havoc_function(const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets)
Generates the havoc function for a function contract.
message_handlert & message_handler
void to_spec_assigns_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively...
const typet & get_target_type(const exprt &expr)
Extracts the type of an assigns clause target expression The expression must be of the form: expr = c...
void generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets)
Translates original_program that specifies assignable targets into a program that havocs the targets.
dfcc_spec_functionst(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
void to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
Base class for all expressions.
A generic container class for the GOTO intermediate representation of one function.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
Dynamic frame condition checking library loading.
dfcc_ptr_havoc_modet
Represents the different ways to havoc pointers.
@ NONDET
havocs the pointer to an nondet pointer
@ INVALID
havocs the pointer to an invalid pointer
Dynamic frame condition checking utility functions.
API to expression classes.