Packages/c/cbmc-doc-6.9.0-1.fc45.x86_64.rpm

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


Module: Validate expressions


Author: Daniel Poetzl


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


#ifndef CPROVER_UTIL_VALIDATE_EXPRESSIONS_H

#define CPROVER_UTIL_VALIDATE_EXPRESSIONS_H


class exprt;

class namespacet;

enum class validation_modet;


void check_expr(const exprt &expr, const validation_modet vm);


void validate_expr(

  const exprt &expr,

  const namespacet &ns,

  const validation_modet vm);


void validate_full_expr(

  const exprt &expr,

  const namespacet &ns,

  const validation_modet vm);


#endif /* CPROVER_UTIL_VALIDATE_EXPRESSIONS_H */

exprt
Base class for all expressions.
Definition expr.h:57

namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91

check_expr
void check_expr(const exprt &expr, const validation_modet vm)
Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its typ...
Definition validate_expressions.cpp:85

validate_full_expr
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
Definition validate_expressions.cpp:114

validate_expr
void validate_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed, assuming that its subexpression and type have already...
Definition validate_expressions.cpp:98

validation_modet
validation_modet
Definition validation_mode.h:13