cprover
Loading...
Searching...
No Matches
contracts.cpp File Reference

Verify and use annotated loop and function contracts. More...

+ Include dependency graph for contracts.cpp:

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.
 
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.
 
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.
 
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.
 

Detailed Description

Verify and use annotated loop and function contracts.

Definition in file contracts.cpp.

Function Documentation

◆ has_disable_assigns_check_pragma()

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.

◆ must_check_assign()

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.

◆ must_track_dead()

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.

◆ must_track_decl()

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.