Weakest Preconditions. More...

#include "wp.h"
#include "goto_instruction_code.h"
#include <util/invariant.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>

Include dependency graph for wp.cpp:

Go to the source code of this file.

Enumerations
enum class	aliasingt { A_MAY , A_MUST , 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.

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

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 &)

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.

Detailed Description

Weakest Preconditions.

Definition in file wp.cpp.

Enumeration Type Documentation

◆ aliasingt

enum class aliasingt

strong

consider possible aliasing

Enumerator
A_MAY
A_MUST
A_MUSTNOT

Definition at line 64 of file wp.cpp.

Function Documentation

◆ aliasing()

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

Definition at line 66 of file wp.cpp.

◆ approximate_nondet()

void approximate_nondet ( exprt & dest )

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

Definition at line 57 of file wp.cpp.

◆ approximate_nondet_rec()

void approximate_nondet_rec	(	exprt &	dest,
		unsigned &	count
	)

Definition at line 42 of file wp.cpp.

◆ has_nondet()

bool has_nondet ( const exprt & dest )

Definition at line 22 of file wp.cpp.

◆ rewrite_assignment()

void rewrite_assignment	(	exprt &	lhs,
		exprt &	rhs
	)

Definition at line 167 of file wp.cpp.

◆ 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 123 of file wp.cpp.

◆ 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 239 of file wp.cpp.

◆ wp_assign()

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

Definition at line 197 of file wp.cpp.

◆ wp_assume()

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

Definition at line 218 of file wp.cpp.

◆ wp_decl()

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

Definition at line 226 of file wp.cpp.

Enumerations

Functions