Skip to content

Commit dd07600

Browse files
committed
Validate class_method_descriptor_exprt thoroughly
In order to ensure we an invalid expression is never constructed or cast to.
1 parent 05930c3 commit dd07600

File tree

1 file changed

+20
-0
lines changed

1 file changed

+20
-0
lines changed

src/util/std_expr.h

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4588,6 +4588,8 @@ inline array_comprehension_exprt &to_array_comprehension_expr(exprt &expr)
45884588
return ret;
45894589
}
45904590

4591+
inline void validate_expr(const class class_method_descriptor_exprt &value);
4592+
45914593
/// An expression describing a method on a class
45924594
class class_method_descriptor_exprt : public nullary_exprt
45934595
{
@@ -4617,6 +4619,7 @@ class class_method_descriptor_exprt : public nullary_exprt
46174619
set(ID_C_class, std::move(class_id));
46184620
set(ID_C_base_name, std::move(base_method_name));
46194621
set(ID_identifier, std::move(id));
4622+
validate_expr(*this);
46204623
}
46214624

46224625
/// The method name after mangling it by combining it with the descriptor.
@@ -4654,6 +4657,23 @@ class class_method_descriptor_exprt : public nullary_exprt
46544657
}
46554658
};
46564659

4660+
inline void validate_expr(const class class_method_descriptor_exprt &value)
4661+
{
4662+
validate_operands(value, 0, "class method descriptor must not have operands");
4663+
DATA_INVARIANT(
4664+
!value.mangled_method_name().empty(),
4665+
"class method descriptor must have a mangled method name.");
4666+
DATA_INVARIANT(
4667+
!value.class_id().empty(), "class method descriptor must have a class id.");
4668+
DATA_INVARIANT(
4669+
!value.base_method_name().empty(),
4670+
"class method descriptor must have a base method name.");
4671+
DATA_INVARIANT(
4672+
value.get_identifier() == id2string(value.class_id()) + "." +
4673+
id2string(value.mangled_method_name()),
4674+
"class method descriptor must have an identifier in the expected format.");
4675+
}
4676+
46574677
/// \brief Cast an exprt to a \ref class_method_descriptor_exprt
46584678
///
46594679
/// \a expr must be known to be \ref class_method_descriptor_exprt.

0 commit comments

Comments
 (0)