cprover
|
Verify and use annotated loop and function contracts. More...
#include "contracts.h"
#include <algorithm>
#include <map>
#include <analyses/local_bitvector_analysis.h>
#include <analyses/local_may_alias.h>
#include <ansi-c/c_expr.h>
#include <goto-instrument/havoc_utils.h>
#include <goto-programs/goto_inline.h>
#include <goto-programs/goto_program.h>
#include <goto-programs/remove_skip.h>
#include <langapi/language_util.h>
#include <util/c_types.h>
#include <util/expr_util.h>
#include <util/find_symbols.h>
#include <util/format_expr.h>
#include <util/fresh_symbol.h>
#include <util/graph.h>
#include <util/mathematical_expr.h>
#include <util/mathematical_types.h>
#include <util/message.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/replace_symbol.h>
#include <util/std_code.h>
#include "havoc_assigns_clause_targets.h"
#include "instrument_spec_assigns.h"
#include "memory_predicates.h"
#include "utils.h"
Go to the source code of this file.
Classes | |
class | inlining_decoratort |
Decorator for message_handlert that keeps track of warnings occuring when inlining a function. More... | |
Functions | |
bool | has_disable_assigns_check_pragma (const goto_programt::const_targett &target) |
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma. More... | |
bool | must_check_assign (const goto_programt::const_targett &target, code_contractst::skipt skip_parameter_assigns, const namespacet ns, const optionalt< cfg_infot > cfg_info_opt) |
Returns true iff an ASSIGN lhs := rhs instruction must be instrumented. More... | |
bool | must_track_decl (const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt) |
Returns true iff a DECL x must be added to the local write set. More... | |
bool | must_track_dead (const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt) |
Returns true iff a DEAD x must be processed to upate the local write set. More... | |
Verify and use annotated loop and function contracts.
Definition in file contracts.cpp.
bool has_disable_assigns_check_pragma | ( | const goto_programt::const_targett & | target | ) |
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma.
Definition at line 1188 of file contracts.cpp.
bool must_check_assign | ( | const goto_programt::const_targett & | target, |
code_contractst::skipt | skip_parameter_assigns, | ||
const namespacet | ns, | ||
const optionalt< cfg_infot > | cfg_info_opt | ||
) |
Returns true iff an ASSIGN lhs := rhs
instruction must be instrumented.
Definition at line 1196 of file contracts.cpp.
bool must_track_dead | ( | const goto_programt::const_targett & | target, |
const optionalt< cfg_infot > & | cfg_info_opt | ||
) |
Returns true iff a DEAD x
must be processed to upate the local write set.
The conditions are the same than for tracking a DECL x
instruction.
Definition at line 1241 of file contracts.cpp.
bool must_track_decl | ( | const goto_programt::const_targett & | target, |
const optionalt< cfg_infot > & | cfg_info_opt | ||
) |
Returns true iff a DECL x
must be added to the local write set.
A variable is called 'dirty' if its address gets taken at some point in the program.
Assuming the goto program is obtained from a structured C program that passed C compiler checks, non-dirty variables can only be assigned to directly by name, cannot escape their lexical scope, and are always safe to assign. Hence, we only track dirty variables in the write set.
Definition at line 1227 of file contracts.cpp.