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

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

◆ has_nondet()

bool has_nondet ( const exprt dest)

◆ rewrite_assignment()

◆ 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(), Forall_operands, irept::id(), 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
codeProgram
postPostcondition
nsNamespace
Returns
Weakest precondition

Definition at line 239 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 197 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 218 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 226 of file wp.cpp.

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

Referenced by wp().