Skip to content

Commit c4bc800

Browse files
committed
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
1 parent c529e7e commit c4bc800

File tree

2 files changed

+0
-66
lines changed

2 files changed

+0
-66
lines changed

src/goto-symex/expr_skeleton.cpp

Lines changed: 0 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -52,51 +52,3 @@ expr_skeletont expr_skeletont::compose(expr_skeletont other) const
5252
{
5353
return expr_skeletont(apply(other.skeleton));
5454
}
55-
56-
/// In the expression corresponding to a skeleton returns a pointer to the
57-
/// deepest subexpression before we encounter nil.
58-
static exprt *deepest_not_nil(exprt &e)
59-
{
60-
exprt *ptr = &e;
61-
while(!ptr->op0().is_nil())
62-
ptr = &ptr->op0();
63-
return ptr;
64-
}
65-
66-
optionalt<expr_skeletont>
67-
expr_skeletont::clear_innermost_index_expr(expr_skeletont skeleton)
68-
{
69-
exprt *to_update = deepest_not_nil(skeleton.skeleton);
70-
if(index_exprt *index_expr = expr_try_dynamic_cast<index_exprt>(*to_update))
71-
{
72-
index_expr->make_nil();
73-
return expr_skeletont{std::move(skeleton)};
74-
}
75-
return {};
76-
}
77-
78-
optionalt<expr_skeletont>
79-
expr_skeletont::clear_innermost_member_expr(expr_skeletont skeleton)
80-
{
81-
exprt *to_update = deepest_not_nil(skeleton.skeleton);
82-
if(member_exprt *member = expr_try_dynamic_cast<member_exprt>(*to_update))
83-
{
84-
member->make_nil();
85-
return expr_skeletont{std::move(skeleton)};
86-
}
87-
return {};
88-
}
89-
90-
optionalt<expr_skeletont>
91-
expr_skeletont::clear_innermost_byte_extract_expr(expr_skeletont skeleton)
92-
{
93-
exprt *to_update = deepest_not_nil(skeleton.skeleton);
94-
if(
95-
to_update->id() != ID_byte_extract_big_endian &&
96-
to_update->id() != ID_byte_extract_little_endian)
97-
{
98-
return {};
99-
}
100-
to_update->make_nil();
101-
return expr_skeletont{std::move(skeleton.skeleton)};
102-
}

src/goto-symex/expr_skeleton.h

Lines changed: 0 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -43,24 +43,6 @@ class expr_skeletont final
4343
/// `array2[index]`.
4444
static expr_skeletont remove_op0(exprt e);
4545

46-
/// If the deepest subexpression in the skeleton is a member expression,
47-
/// replace it with a nil expression and return the obtained skeleton.
48-
static optionalt<expr_skeletont>
49-
clear_innermost_index_expr(expr_skeletont skeleton);
50-
51-
/// If the deepest subexpression in the skeleton is a member expression,
52-
/// replace it with a nil expression and return the obtained skeleton.
53-
static optionalt<expr_skeletont>
54-
clear_innermost_member_expr(expr_skeletont skeleton);
55-
56-
/// If the deepest subexpression in the skeleton is a byte-extract expression,
57-
/// replace it with a nil expression and return the obtained skeleton.
58-
/// For instance, for `(byte_extract(☐, 2, int)).field[index]`
59-
/// `☐.field[index]` is returned, while for `byte_extract(☐.field, 2, int)`
60-
/// an empty optional is returned.
61-
static optionalt<expr_skeletont>
62-
clear_innermost_byte_extract_expr(expr_skeletont skeleton);
63-
6446
private:
6547
/// In \c skeleton, nil_exprt is used to mark the sub expression to be
6648
/// substituted. The nil_exprt always appears recursively following the first

0 commit comments

Comments
 (0)