cprover
|
Expression in which some part is missing and can be substituted for another expression. More...
#include <expr_skeleton.h>
Public Member Functions | |
expr_skeletont () | |
Empty skeleton. | |
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. | |
exprt | apply (exprt expr) const |
Replace the missing part by the given expression, to end-up with a complete expression. |
Static Public Member Functions | |
static expr_skeletont | remove_op0 (exprt e) |
Create a skeleton by removing the first operand of e . |
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. |
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.
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.
|
inlineexplicitprivate |
Definition at line 53 of file expr_skeleton.h.
Replace the missing part by the given expression, to end-up with a complete expression.
Definition at line 28 of file expr_skeleton.cpp.
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.
|
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.
|
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.