cprover
wp.h File Reference

Weakest Preconditions. More...

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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...
 
void approximate_nondet (exprt &dest)
 approximate the non-deterministic choice in a way cheaper than by (proper) quantification More...
 

Detailed Description

Weakest Preconditions.

Definition in file wp.h.

Function Documentation

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

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