12 #ifndef CPROVER_GOTO_PROGRAMS_WP_H 13 #define CPROVER_GOTO_PROGRAMS_WP_H 37 #endif // CPROVER_GOTO_PROGRAMS_WP_H A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void approximate_nondet(exprt &dest)
approximate the non-deterministic choice in a way cheaper than by (proper) quantification ...
Base class for all expressions.
Data structure for representing an arbitrary statement in a program.
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...