wp.cpp File Reference

Weakest Preconditions. More...

#include "wp.h"
#include <util/std_expr.h>
#include <util/std_code.h>
#include <util/base_type.h>

Include dependency graph for wp.cpp:

Go to the source code of this file.

Enumerations
enum	aliasingt { aliasingt::A_MAY, aliasingt::A_MUST, aliasingt::A_MUSTNOT }
	consider possible aliasing More...

Functions
bool	has_nondet (const exprt &dest)
void	approximate_nondet_rec (exprt &dest, unsigned &count)
void	approximate_nondet (exprt &dest)
	approximate the non-deterministic choice in a way cheaper than by (proper) quantification More...
aliasingt	aliasing (const exprt &e1, const exprt &e2, const namespacet &ns)
void	substitute_rec (exprt &dest, const exprt &what, const exprt &by, const namespacet &ns)
	replace 'what' by 'by' in 'dest', considering possible aliasing More...
void	rewrite_assignment (exprt &lhs, exprt &rhs)
exprt	wp_assign (const code_assignt &code, const exprt &post, const namespacet &ns)
exprt	wp_assume (const code_assumet &code, const exprt &post, const namespacet &ns)
exprt	wp_decl (const code_declt &code, const exprt &post, const namespacet &ns)
exprt	wp (const codet &code, const exprt &post, const namespacet &ns)
	Compute the weakest precondition of the given program piece code with respect to the expression post. More...

Detailed Description

Weakest Preconditions.

Definition in file wp.cpp.

Enumeration Type Documentation

aliasingt

enum aliasingt

strong

consider possible aliasing

Enumerator
A_MAY
A_MUST
A_MUSTNOT

Definition at line 60 of file wp.cpp.

Function Documentation

aliasing()

aliasingt aliasing	(	const exprt &	e1,
		const exprt &	e2,
		const namespacet &	ns
	)

Definition at line 62 of file wp.cpp.

References A_MAY, A_MUST, A_MUSTNOT, base_type_eq(), symbol_exprt::get_identifier(), irept::id(), exprt::op0(), exprt::operands(), to_symbol_expr(), and exprt::type().

Referenced by substitute_rec().

approximate_nondet()

void approximate_nondet

(

exprt &

dest

)

approximate the non-deterministic choice in a way cheaper than by (proper) quantification

Definition at line 53 of file wp.cpp.

References approximate_nondet_rec().

Referenced by wp_assign().

approximate_nondet_rec()

void approximate_nondet_rec	(	exprt &	dest,
		unsigned &	count
	)

Definition at line 38 of file wp.cpp.

References Forall_operands, side_effect_exprt::get_statement(), irept::id(), irept::set(), and to_side_effect_expr().

Referenced by approximate_nondet().

has_nondet()

bool has_nondet

(

const exprt &

dest

)

Definition at line 20 of file wp.cpp.

References forall_operands, side_effect_exprt::get_statement(), irept::id(), and to_side_effect_expr().

rewrite_assignment()

void rewrite_assignment	(	exprt &	lhs,
		exprt &	rhs
	)

Definition at line 164 of file wp.cpp.

References index_exprt::array(), member_exprt::get_component_name(), irept::id(), index_exprt::index(), with_exprt::new_value(), with_exprt::old(), irept::set(), member_exprt::struct_op(), to_index_expr(), to_member_expr(), exprt::type(), and with_exprt::where().

Referenced by wp_assign().

substitute_rec()

void substitute_rec	(	exprt &	dest,
		const exprt &	what,
		const exprt &	by,
		const namespacet &	ns
	)

replace 'what' by 'by' in 'dest', considering possible aliasing

Definition at line 115 of file wp.cpp.

References A_MAY, A_MUST, A_MUSTNOT, aliasing(), if_exprt::cond(), if_exprt::false_case(), Forall_operands, irept::id(), if_exprt::true_case(), and exprt::type().

Referenced by wp_assign().

wp()

exprt wp	(	const codet &	code,
		const exprt &	post,
		const namespacet &	ns
	)

Compute the weakest precondition of the given program piece code with respect to the expression post.

Parameters

code	Program
post	Postcondition
ns	Namespace

Returns

Weakest precondition

Definition at line 244 of file wp.cpp.

References codet::get_statement(), id2string(), to_code_assign(), to_code_assume(), to_code_decl(), wp_assign(), wp_assume(), and wp_decl().

wp_assign()

exprt wp_assign	(	const code_assignt &	code,
		const exprt &	post,
		const namespacet &	ns
	)

Definition at line 202 of file wp.cpp.

References approximate_nondet(), code_assignt::lhs(), rewrite_assignment(), code_assignt::rhs(), and substitute_rec().

Referenced by wp(), and wp_decl().

wp_assume()

exprt wp_assume	(	const code_assumet &	code,
		const exprt &	post,
		const namespacet &	ns
	)

Definition at line 223 of file wp.cpp.

References code_assumet::assumption().

Referenced by wp().

wp_decl()

exprt wp_decl	(	const code_declt &	code,
		const exprt &	post,
		const namespacet &	ns
	)

Definition at line 231 of file wp.cpp.

References code_declt::symbol(), exprt::type(), and wp_assign().

Referenced by wp().