CBMC
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 
25 exprt wp(
26  const codet &code,
27  const exprt &post,
28  const namespacet &ns);
29 
32 void approximate_nondet(exprt &dest);
33 
34 #endif // CPROVER_GOTO_PROGRAMS_WP_H
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt
Base class for all expressions.
Definition: expr.h:56
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
approximate_nondet
void approximate_nondet(exprt &dest)
Approximate the non-deterministic choice in a way cheaper than by (proper) quantification.
Definition: wp.cpp:57
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.
Definition: wp.cpp:239