Expression in which some part is missing and can be substituted for another expression. More...
#include <expr_skeleton.h>
Collaboration diagram for expr_skeletont:Public Member Functions | |
| expr_skeletont () | |
| Empty skeleton. More... | |
| expr_skeletont | compose (expr_skeletont other) const |
| Replace the missing part of the current skeleton by another skeleton, ending in a bigger skeleton corresponding to the two combined. More... | |
| exprt | apply (exprt expr) const |
| Replace the missing part by the given expression, to end-up with a complete expression. More... | |
Static Public Member Functions | |
| static expr_skeletont | remove_op0 (exprt e) |
Create a skeleton by removing the first operand of e. More... | |
Private Member Functions | |
| expr_skeletont (exprt e) | |
Private Attributes | |
| exprt | skeleton |
In skeleton, nil_exprt is used to mark the sub expression to be substituted. More... | |
Detailed Description
Expression in which some part is missing and can be substituted for another expression.
For instance, a skeleton ☐[index] where ☐ is the missing part, can be applied to an expression x to get x[index] (see expr_skeletont::apply). It can also be composed with another skeleton, let say ☐.some_field which would give the skeleton ☐.some_field[index] (see expr_skeletont::compose).
Definition at line 25 of file expr_skeleton.h.
Constructor & Destructor Documentation
◆ expr_skeletont() [1/2]
| expr_skeletont::expr_skeletont | ( | ) |
Empty skeleton.
Applying it to an expression would give the same expression unchanged
Definition at line 16 of file expr_skeleton.cpp.
◆ expr_skeletont() [2/2]
|
inlineexplicitprivate |
Definition at line 53 of file expr_skeleton.h.
Member Function Documentation
◆ apply()
Replace the missing part by the given expression, to end-up with a complete expression.
Definition at line 28 of file expr_skeleton.cpp.
◆ compose()
| expr_skeletont expr_skeletont::compose | ( | expr_skeletont | other | ) | const |
Replace the missing part of the current skeleton by another skeleton, ending in a bigger skeleton corresponding to the two combined.
Definition at line 51 of file expr_skeleton.cpp.
◆ remove_op0()
|
static |
Create a skeleton by removing the first operand of e.
For instance, remove_op0 on array[index] would give a skeleton in which array is missing, and applying that skeleton to array2 would give array2[index].
Definition at line 20 of file expr_skeleton.cpp.
Member Data Documentation
◆ skeleton
|
private |
In skeleton, nil_exprt is used to mark the sub expression to be substituted.
The nil_exprt always appears recursively following the first operands because the only way to get a skeleton is by removing the first operand.
Definition at line 51 of file expr_skeleton.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-symex/expr_skeleton.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-symex/expr_skeleton.cpp
