code_contracts.cpp File Reference

Verify and use annotated invariants and pre/post-conditions. More...

#include "code_contracts.h"
#include <util/cprover_prefix.h>
#include <util/fresh_symbol.h>
#include <util/replace_symbol.h>
#include <goto-programs/remove_skip.h>
#include <analyses/local_may_alias.h>
#include "loop_utils.h"

Include dependency graph for code_contracts.cpp:

Go to the source code of this file.

Classes
class	code_contractst

Functions
static void	check_apply_invariants (goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop)
void	code_contracts (symbol_tablet &symbol_table, goto_functionst &goto_functions)

Detailed Description

Verify and use annotated invariants and pre/post-conditions.

Definition in file code_contracts.cpp.

Function Documentation

check_apply_invariants()

static void check_apply_invariants ( goto_functionst::goto_functiont &  goto_function, const local_may_aliast &  local_may_alias, const goto_programt::targett  loop_head, const loopt &  loop  )

static

Definition at line 66 of file code_contracts.cpp.

References goto_program_templatet< codeT, guardT >::add_instruction(), ASSERT, ASSUME, build_havoc_code(), get_modifies(), GOTO, irept::is_nil(), source_locationt::set_comment(), and exprt::source_location().

Referenced by code_contractst::code_contracts().

code_contracts()

void code_contracts	(	symbol_tablet &	symbol_table,
		goto_functionst &	goto_functions
	)

Definition at line 403 of file code_contracts.cpp.

Referenced by goto_instrument_parse_optionst::instrument_goto_program().