cprover
wp.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Weakest Preconditions
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_WP_H
13 #define CPROVER_GOTO_PROGRAMS_WP_H
14 
15 class codet;
16 class exprt;
17 class namespacet;
18 
26 exprt wp(
27  const codet &code,
28  const exprt &post,
29  const namespacet &ns);
30 
35 void approximate_nondet(exprt &dest);
36 
37 #endif // CPROVER_GOTO_PROGRAMS_WP_H
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void approximate_nondet(exprt &dest)
approximate the non-deterministic choice in a way cheaper than by (proper) quantification ...
Definition: wp.cpp:53
Base class for all expressions.
Definition: expr.h:46
A statement in a programming language.
Definition: std_code.h:19
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...
Definition: wp.cpp:244