cprover
|
Instrument Contracts. More...
#include "instrument_contracts.h"
#include <util/c_types.h>
#include <util/mathematical_expr.h>
#include <util/pointer_predicates.h>
#include <util/prefix.h>
#include <util/replace_symbol.h>
#include <util/std_code.h>
#include <goto-programs/goto_model.h>
#include <ansi-c/expr2c.h>
Go to the source code of this file.
Macros | |
#define | MAX_TEXT 20 |
Instrument Contracts.
Definition in file instrument_contracts.cpp.
#define MAX_TEXT 20 |
Definition at line 25 of file instrument_contracts.cpp.
Definition at line 74 of file instrument_contracts.cpp.
source_locationt add_function | ( | irep_idt | function_identifier, |
source_locationt | src ) |
Definition at line 65 of file instrument_contracts.cpp.
Definition at line 107 of file instrument_contracts.cpp.
|
static |
Definition at line 44 of file instrument_contracts.cpp.
symbol_exprt find_old_expr | ( | const exprt & | src, |
const std::string & | prefix, | ||
std::vector< std::pair< symbol_exprt, exprt > > & | old_exprs ) |
Definition at line 213 of file instrument_contracts.cpp.
optionalt< code_with_contract_typet > get_contract | ( | const irep_idt & | function_identifier, |
const namespacet & | ns ) |
Definition at line 28 of file instrument_contracts.cpp.
bool has_contract | ( | const irep_idt & | function_identifier, |
const namespacet & | ns ) |
Definition at line 39 of file instrument_contracts.cpp.
Definition at line 138 of file instrument_contracts.cpp.
void instrument_contract_checks | ( | goto_functionst::function_mapt::value_type & | f, |
const namespacet & | ns ) |
Definition at line 268 of file instrument_contracts.cpp.
void instrument_contracts | ( | goto_modelt & | goto_model | ) |
Definition at line 554 of file instrument_contracts.cpp.
Definition at line 202 of file instrument_contracts.cpp.
Definition at line 184 of file instrument_contracts.cpp.
Definition at line 97 of file instrument_contracts.cpp.
Definition at line 53 of file instrument_contracts.cpp.
|
static |
Definition at line 143 of file instrument_contracts.cpp.
goto_programt old_assignments | ( | const std::vector< std::pair< symbol_exprt, exprt > > & | old_exprs, |
const source_locationt & | source_location ) |
Definition at line 250 of file instrument_contracts.cpp.
void replace_function_calls_by_contracts | ( | goto_functionst::function_mapt::value_type & | f, |
const goto_modelt & | goto_model ) |
Definition at line 394 of file instrument_contracts.cpp.
exprt replace_old | ( | exprt | src, |
const std::string & | prefix, | ||
std::vector< std::pair< symbol_exprt, exprt > > & | old_exprs ) |
Definition at line 231 of file instrument_contracts.cpp.
exprt replace_source_location | ( | exprt | src, |
const source_locationt & | source_location ) |
Definition at line 85 of file instrument_contracts.cpp.