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 "pointer_expr.h"
17 #include "ssa_expr.h"
18 
19 #define CALL_ON_EXPR(expr_type) \
20  C<exprt, expr_type>()(expr, std::forward<Args>(args)...)
21 
22 template <template <typename, typename> class C, typename... Args>
23 void call_on_expr(const exprt &expr, Args &&... args)
24 {
25  if(expr.id() == ID_equal)
26  {
28  }
29  else if(expr.id() == ID_plus)
30  {
32  }
33  else if(is_ssa_expr(expr))
34  {
36  }
37  else if(expr.id() == ID_member)
38  {
40  }
41  else if(expr.id() == ID_dereference)
42  {
44  }
45  else
46  {
47 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
48  std::cerr << "Unimplemented well-formedness check for expression with id: "
49  << expr.id_string() std::endl;
50 #endif
51 
53  }
54 }
55 
64 void check_expr(const exprt &expr, const validation_modet vm)
65 {
66  call_on_expr<call_checkt>(expr, vm);
67 }
68 
78  const exprt &expr,
79  const namespacet &ns,
80  const validation_modet vm)
81 {
82  call_on_expr<call_validatet>(expr, ns, vm);
83 }
84 
94  const exprt &expr,
95  const namespacet &ns,
96  const validation_modet vm)
97 {
98  call_on_expr<call_validate_fullt>(expr, ns, vm);
99 }
Operator to dereference a pointer.
Definition: pointer_expr.h:648
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const std::string & id_string() const
Definition: irep.h:399
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The plus expression Associativity is not specified.
Definition: std_expr.h:914
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
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