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
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:74
approximate_nondet
void approximate_nondet(exprt &dest)
approximate the non-deterministic choice in a way cheaper than by (proper) quantification ...
Definition:
wp.cpp:53
exprt
Base class for all expressions.
Definition:
expr.h:42
codet
A statement in a programming language.
Definition:
std_code.h:21
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
goto-programs
wp.h
Generated by
1.8.14