cbmc/wp_8h_source.html

/*******************************************************************\


Module: Weakest Preconditions


Author: Daniel Kroening, kroening@kroening.com


\*******************************************************************/


#ifndef CPROVER_GOTO_PROGRAMS_WP_H

#define CPROVER_GOTO_PROGRAMS_WP_H


class codet;

class exprt;

class namespacet;


exprt wp(

  const codet &code,

  const exprt &post,

  const namespacet &ns);


void approximate_nondet(exprt &dest);


#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:91

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