diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc deleted file mode 100644 index 74fb1af96136..000000000000 --- a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc +++ /dev/null @@ -1,11 +0,0 @@ -CORE -Test ---function Test.main --no-simplify --unwind 10 --show-vcc -^EXIT=0$ -^SIGNAL=0$ -"java::Impl1" = cast\(\{ \{ "java::Impl1" \}, 0 \}, struct (\{ struct \{ string @class_identifier \} @java.lang.Object \}|java::Intf)\)\.@java.lang.Object\.@class_identifier --- -^warning: ignoring --- -This checks that the test generates the VCC testing the class-id that we're -intending to simplify away in the main test. diff --git a/regression/cbmc/struct2/main.c b/regression/cbmc/struct2/main.c new file mode 100644 index 000000000000..0f2c38670328 --- /dev/null +++ b/regression/cbmc/struct2/main.c @@ -0,0 +1,24 @@ +struct T +{ + // intentionally empty to trigger is_prefix_of code (empty structs, however, + // are a GCC-only feature) +}; + +struct S +{ + struct T t; + int other; +}; + +void foo(struct S s2) +{ + struct T *p = &s2.t; + struct T t2 = *p; + __CPROVER_assert(0, ""); +} + +int main() +{ + struct S s; + foo(s); +} diff --git a/regression/cbmc/struct2/test.desc b/regression/cbmc/struct2/test.desc new file mode 100644 index 000000000000..f46890667749 --- /dev/null +++ b/regression/cbmc/struct2/test.desc @@ -0,0 +1,11 @@ +CORE gcc-only broken-smt-backend +main.c + +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test must not generate a warning about typecasts (between different struct +types) being ignored. diff --git a/regression/cbmc/struct5/main.c b/regression/cbmc/struct5/main.c new file mode 100644 index 000000000000..ca759d39b546 --- /dev/null +++ b/regression/cbmc/struct5/main.c @@ -0,0 +1,28 @@ +#include + +struct a +{ + int x; +}; +struct b +{ + struct a p; + int y; +}; + +int f00(struct a *ptr) +{ + return ptr->x; +} + +int main() +{ + struct b z = {{1}, 2}; + + assert(&z == &(z.p)); + assert(&z == &(z.p.x)); + + assert(f00(&z) == z.p.x); + + return 0; +} diff --git a/regression/cbmc/struct5/test.desc b/regression/cbmc/struct5/test.desc new file mode 100644 index 000000000000..278f468e1305 --- /dev/null +++ b/regression/cbmc/struct5/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 01c5710a53ab..eabad1b62e38 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -368,19 +368,6 @@ bool value_set_dereferencet::dereference_type_compare( if(object_type == dereference_type) return true; // ok, they just match - // check for struct prefixes - - const typet ot_base=ns.follow(object_type), - dt_base=ns.follow(dereference_type); - - if(ot_base.id()==ID_struct && - dt_base.id()==ID_struct) - { - if(to_struct_type(dt_base).is_prefix_of( - to_struct_type(ot_base))) - return true; // ok, dt is a prefix of ot - } - // we are generous about code pointers if(dereference_type.id()==ID_code && object_type.id()==ID_code) diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 117c7672ffa7..079dc74c817a 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -110,35 +110,6 @@ optionalt struct_typet::get_base(const irep_idt &id) const return {}; } -/// Returns true if the struct is a prefix of \a other, i.e., if this struct -/// has n components then the component types and names of this struct must -/// match the first n components of \a other struct. -/// \param other: Struct type to compare with. -bool struct_typet::is_prefix_of(const struct_typet &other) const -{ - const componentst &ot_components=other.components(); - const componentst &tt_components=components(); - - if(ot_components.size()< - tt_components.size()) - return false; - - componentst::const_iterator - ot_it=ot_components.begin(); - - for(const auto &tt_c : tt_components) - { - if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name()) - { - return false; // they just don't match - } - - ot_it++; - } - - return true; // ok, *this is a prefix of ot -} - /// Returns true if the type is a reference. bool is_reference(const typet &type) { diff --git a/src/util/std_types.h b/src/util/std_types.h index 3ed8f5142353..d1fab6681b8c 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -239,8 +239,6 @@ class struct_typet:public struct_union_typet { } - bool is_prefix_of(const struct_typet &other) const; - /// A struct may be a class, where members may have access restrictions. bool is_class() const {