replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Remove now-unnecessary expr_skeletont methods 

These are unused now that we don't have shift_indexed_access_to_lhs or rewrite_with_to_field_symbols
This commit is contained in:
Chris Smowton 2019-07-24 14:31:03 +01:00
parent c529e7e01e
commit c4bc80029d
2 changed files with 0 additions and 66 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
src/goto-symex/expr_skeleton.cpp
View File

@ -52,51 +52,3 @@ expr_skeletont expr_skeletont::compose(expr_skeletont other) const
{
return expr_skeletont(apply(other.skeleton));
}
/// In the expression corresponding to a skeleton returns a pointer to the
/// deepest subexpression before we encounter nil.
static exprt *deepest_not_nil(exprt &e)
{
exprt *ptr = &e;
while(!ptr->op0().is_nil())
ptr = &ptr->op0();
return ptr;
}
optionalt<expr_skeletont>
expr_skeletont::clear_innermost_index_expr(expr_skeletont skeleton)
{
exprt *to_update = deepest_not_nil(skeleton.skeleton);
if(index_exprt *index_expr = expr_try_dynamic_cast<index_exprt>(*to_update))
{
index_expr->make_nil();
return expr_skeletont{std::move(skeleton)};
}
return {};
}
optionalt<expr_skeletont>
expr_skeletont::clear_innermost_member_expr(expr_skeletont skeleton)
{
exprt *to_update = deepest_not_nil(skeleton.skeleton);
if(member_exprt *member = expr_try_dynamic_cast<member_exprt>(*to_update))
{
member->make_nil();
return expr_skeletont{std::move(skeleton)};
}
return {};
}
optionalt<expr_skeletont>
expr_skeletont::clear_innermost_byte_extract_expr(expr_skeletont skeleton)
{
exprt *to_update = deepest_not_nil(skeleton.skeleton);
if(
to_update->id() != ID_byte_extract_big_endian &&
to_update->id() != ID_byte_extract_little_endian)
{
return {};
}
to_update->make_nil();
return expr_skeletont{std::move(skeleton.skeleton)};
}

18
src/goto-symex/expr_skeleton.h
View File

@ -43,24 +43,6 @@ public:
/// `array2[index]`.
static expr_skeletont remove_op0(exprt e);
/// If the deepest subexpression in the skeleton is a member expression,
/// replace it with a nil expression and return the obtained skeleton.
static optionalt<expr_skeletont>
clear_innermost_index_expr(expr_skeletont skeleton);
/// If the deepest subexpression in the skeleton is a member expression,
/// replace it with a nil expression and return the obtained skeleton.
static optionalt<expr_skeletont>
clear_innermost_member_expr(expr_skeletont skeleton);
/// If the deepest subexpression in the skeleton is a byte-extract expression,
/// replace it with a nil expression and return the obtained skeleton.
/// For instance, for `(byte_extract(☐, 2, int)).field[index]`
/// `☐.field[index]` is returned, while for `byte_extract(☐.field, 2, int)`
/// an empty optional is returned.
static optionalt<expr_skeletont>
clear_innermost_byte_extract_expr(expr_skeletont skeleton);
private:
/// In \c skeleton, nil_exprt is used to mark the sub expression to be
/// substituted. The nil_exprt always appears recursively following the first