CBMC
validate_expressions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Validate expressions
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_VALIDATE_EXPRESSIONS_H
10 #define CPROVER_UTIL_VALIDATE_EXPRESSIONS_H
11 
12 class exprt;
13 class namespacet;
14 enum class validation_modet;
15 
16 void check_expr(const exprt &expr, const validation_modet vm);
17 
18 void validate_expr(
19  const exprt &expr,
20  const namespacet &ns,
21  const validation_modet vm);
22 
23 void validate_full_expr(
24  const exprt &expr,
25  const namespacet &ns,
26  const validation_modet vm);
27 
28 #endif /* CPROVER_UTIL_VALIDATE_EXPRESSIONS_H */
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
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