CBMC
expr_skeleton.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_EXPR_SKELETON_H
13 #define CPROVER_GOTO_SYMEX_EXPR_SKELETON_H
14 
15 #include <util/expr.h>
16 
25 class expr_skeletont final
26 {
27 public:
30  expr_skeletont();
31 
34  expr_skeletont compose(expr_skeletont other) const;
35 
38  exprt apply(exprt expr) const;
39 
44  static expr_skeletont remove_op0(exprt e);
45 
46 private:
51  exprt skeleton;
52 
53  explicit expr_skeletont(exprt e) : skeleton(std::move(e))
54  {
55  }
56 };
57 
58 #endif // CPROVER_GOTO_SYMEX_EXPR_SKELETON_H
expr_skeletont
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
expr_skeletont::apply
exprt apply(exprt expr) const
Replace the missing part by the given expression, to end-up with a complete expression.
Definition: expr_skeleton.cpp:28
expr_skeletont::expr_skeletont
expr_skeletont(exprt e)
Definition: expr_skeleton.h:53
expr_skeletont::expr_skeletont
expr_skeletont()
Empty skeleton.
Definition: expr_skeleton.cpp:16
expr_skeletont::compose
expr_skeletont compose(expr_skeletont other) const
Replace the missing part of the current skeleton by another skeleton, ending in a bigger skeleton cor...
Definition: expr_skeleton.cpp:51
expr_skeletont::remove_op0
static expr_skeletont remove_op0(exprt e)
Create a skeleton by removing the first operand of e.
Definition: expr_skeleton.cpp:20
expr_skeletont::skeleton
exprt skeleton
In skeleton, nil_exprt is used to mark the sub expression to be substituted.
Definition: expr_skeleton.h:51
exprt
Base class for all expressions.
Definition: expr.h:56