cprover
validate_expressions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Validate expressions
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
9 #include "validate_expressions.h"
10 #include "validate_helpers.h"
11 
12 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
13 #include <iostream>
14 #endif
15 
16 #include "expr.h"
17 #include "namespace.h"
18 #include "pointer_expr.h"
19 #include "ssa_expr.h"
20 #include "std_expr.h"
21 #include "validate.h"
22 
23 #define CALL_ON_EXPR(expr_type) \
24  C<exprt, expr_type>()(expr, std::forward<Args>(args)...)
25 
26 template <template <typename, typename> class C, typename... Args>
27 void call_on_expr(const exprt &expr, Args &&... args)
28 {
29  if(expr.id() == ID_equal)
30  {
32  }
33  else if(expr.id() == ID_plus)
34  {
36  }
37  else if(is_ssa_expr(expr))
38  {
40  }
41  else if(expr.id() == ID_member)
42  {
44  }
45  else if(expr.id() == ID_dereference)
46  {
48  }
49  else
50  {
51 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
52  std::cerr << "Unimplemented well-formedness check for expression with id: "
53  << expr.id_string() std::endl;
54 #endif
55 
57  }
58 }
59 
68 void check_expr(const exprt &expr, const validation_modet vm)
69 {
70  call_on_expr<call_checkt>(expr, vm);
71 }
72 
82  const exprt &expr,
83  const namespacet &ns,
84  const validation_modet vm)
85 {
86  call_on_expr<call_validatet>(expr, ns, vm);
87 }
88 
98  const exprt &expr,
99  const namespacet &ns,
100  const validation_modet vm)
101 {
102  call_on_expr<call_validate_fullt>(expr, ns, vm);
103 }
Operator to dereference a pointer.
Definition: pointer_expr.h:256
Equality.
Definition: std_expr.h:1140
Base class for all expressions.
Definition: expr.h:54
const std::string & id_string() const
Definition: irep.h:410
const irep_idt & id() const
Definition: irep.h:407
Extract member of struct or union.
Definition: std_expr.h:2528
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The plus expression Associativity is not specified.
Definition: std_expr.h:831
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
API to expression classes for Pointers.
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
API to expression classes.
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...
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...
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...
void call_on_expr(const exprt &expr, Args &&... args)
#define CALL_ON_EXPR(expr_type)
validation_modet