From d79067e568859789f9f31425cfcaa62167e27ecb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 7 Apr 2017 13:33:15 +0100 Subject: [PATCH 1/4] Remove long-deprecated c_sizeof in favour of size_of_expr et al. --- src/ansi-c/Makefile | 1 - src/ansi-c/c_sizeof.cpp | 320 -------------------------- src/ansi-c/c_sizeof.h | 51 ---- src/ansi-c/c_typecheck_expr.cpp | 12 +- src/ansi-c/c_typecheck_type.cpp | 3 +- src/cpp/cpp_typecheck_expr.cpp | 6 +- src/cpp/cpp_typecheck_initializer.cpp | 8 +- src/goto-instrument/stack_depth.cpp | 1 + src/util/pointer_offset_size.cpp | 67 ++++-- 9 files changed, 60 insertions(+), 409 deletions(-) delete mode 100644 src/ansi-c/c_sizeof.cpp delete mode 100644 src/ansi-c/c_sizeof.h diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index f251dc3910c..58dd5b46025 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -14,7 +14,6 @@ SRC = anonymous_member.cpp \ c_nondet_symbol_factory.cpp \ c_preprocess.cpp \ c_qualifiers.cpp \ - c_sizeof.cpp \ c_storage_spec.cpp \ c_typecast.cpp \ c_typecheck_argc_argv.cpp \ diff --git a/src/ansi-c/c_sizeof.cpp b/src/ansi-c/c_sizeof.cpp deleted file mode 100644 index fad6d00ce9f..00000000000 --- a/src/ansi-c/c_sizeof.cpp +++ /dev/null @@ -1,320 +0,0 @@ -/*******************************************************************\ - -Module: Conversion of sizeof Expressions - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Conversion of sizeof Expressions - -#include "c_sizeof.h" - -#include -#include -#include -#include -#include - -#include "c_typecast.h" - -exprt c_sizeoft::sizeof_rec(const typet &type) -{ - // this implementation will eventually be replaced - // by size_of_expr in util/pointer_offset_size.h - exprt dest; - - if(type.id()==ID_signedbv || - type.id()==ID_unsignedbv || - type.id()==ID_floatbv || - type.id()==ID_fixedbv || - type.id()==ID_c_bool) - { - // We round up to bytes. - // See special treatment for bit-fields below. - std::size_t bits=to_bitvector_type(type).get_width(); - std::size_t bytes=bits/8; - if((bits%8)!=0) - bytes++; - dest=from_integer(bytes, size_type()); - } - else if(type.id()==ID_incomplete_c_enum) - { - // refuse to give a size - return nil_exprt(); - } - else if(type.id()==ID_c_enum) - { - // check the subtype - dest=sizeof_rec(type.subtype()); - } - else if(type.id()==ID_c_enum_tag) - { - // follow the tag - dest=sizeof_rec(ns.follow_tag(to_c_enum_tag_type(type))); - } - else if(type.id()==ID_pointer) - { - // the following is an MS extension - if(type.get_bool(ID_C_ptr32)) - return from_integer(4, size_type()); - - std::size_t bits=config.ansi_c.pointer_width; - std::size_t bytes=bits/8; - if((bits%8)!=0) - bytes++; - dest=from_integer(bytes, size_type()); - } - else if(type.id()==ID_bool) - { - // We fit booleans into a byte. - // Don't confuse with c_bool, which is a bit-vector type. - dest=from_integer(1, size_type()); - } - else if(type.id()==ID_array) - { - const exprt &size_expr= - to_array_type(type).size(); - - if(size_expr.is_nil()) - { - // treated like an empty array - dest=from_integer(0, size_type()); - } - else - { - exprt tmp_dest=sizeof_rec(type.subtype()); - - if(tmp_dest.is_nil()) - return tmp_dest; - - mp_integer a, b; - - if(!to_integer(tmp_dest, a) && - !to_integer(size_expr, b)) - { - dest=from_integer(a*b, size_type()); - } - else - { - dest.id(ID_mult); - dest.type()=size_type(); - dest.copy_to_operands(size_expr); - dest.move_to_operands(tmp_dest); - c_implicit_typecast(dest.op0(), dest.type(), ns); - c_implicit_typecast(dest.op1(), dest.type(), ns); - } - } - } - else if(type.id()==ID_struct) - { - const struct_typet::componentst &components= - to_struct_type(type).components(); - - dest=from_integer(0, size_type()); - - mp_integer bit_field_width=0; - - for(const auto &comp : components) - { - const typet &sub_type=ns.follow(comp.type()); - - if(comp.get_bool(ID_is_type)) - { - } - else if(sub_type.id()==ID_code) - { - } - else if(sub_type.id()==ID_c_bit_field) - { - // We just sum them up. - // This assumes they are properly padded. - bit_field_width+=to_c_bit_field_type(sub_type).get_width(); - } - else - { - exprt tmp=sizeof_rec(sub_type); - - if(tmp.is_nil()) - return tmp; - - dest=plus_exprt(dest, tmp); - } - } - - if(bit_field_width!=0) - dest=plus_exprt(dest, from_integer(bit_field_width/8, size_type())); - } - else if(type.id()==ID_union) - { - // the empty union will have size 0 - exprt max_size=from_integer(0, size_type()); - - const union_typet::componentst &components= - to_union_type(type).components(); - - for(const auto &comp : components) - { - if(comp.get_bool(ID_is_type) || comp.type().id()==ID_code) - continue; - - const typet &sub_type=comp.type(); - - exprt tmp; - - if(sub_type.id()==ID_c_bit_field) - { - std::size_t width=to_c_bit_field_type(sub_type).get_width(); - tmp= - from_integer(width/8, size_type()); - } - else - { - tmp=sizeof_rec(sub_type); - - if(tmp.is_nil()) - return nil_exprt(); - } - - max_size=if_exprt( - binary_relation_exprt(max_size, ID_lt, tmp), - tmp, max_size); - - simplify(max_size, ns); - } - - dest=max_size; - } - else if(type.id()==ID_symbol) - { - return sizeof_rec(ns.follow(type)); - } - else if(type.id()==ID_empty) - { - // gcc says that sizeof(void)==1, ISO C doesn't - dest=from_integer(1, size_type()); - } - else if(type.id()==ID_vector) - { - // simply multiply - const exprt &size_expr= - to_vector_type(type).size(); - - exprt tmp_dest=sizeof_rec(type.subtype()); - - if(tmp_dest.is_nil()) - return tmp_dest; - - mp_integer a, b; - - if(!to_integer(tmp_dest, a) && - !to_integer(size_expr, b)) - { - dest=from_integer(a*b, size_type()); - } - else - { - dest.id(ID_mult); - dest.type()=size_type(); - dest.copy_to_operands(size_expr); - dest.move_to_operands(tmp_dest); - c_implicit_typecast(dest.op0(), dest.type(), ns); - c_implicit_typecast(dest.op1(), dest.type(), ns); - } - } - else if(type.id()==ID_complex) - { - // this is a pair - - exprt tmp_dest=sizeof_rec(type.subtype()); - - if(tmp_dest.is_nil()) - return tmp_dest; - - mp_integer a; - - if(!to_integer(tmp_dest, a)) - dest=from_integer(a*2, size_type()); - else - return nil_exprt(); - } - else - { - // We give up; this shouldn't really happen on 'proper' C types, - // but we do have some artificial ones that simply have no - // meaningful size. - dest.make_nil(); - } - - return dest; -} - -exprt c_sizeoft::c_offsetof( - const struct_typet &type, - const irep_idt &component_name) -{ - const struct_typet::componentst &components= - type.components(); - - exprt dest=from_integer(0, size_type()); - - mp_integer bit_field_width=0; - - for(const auto &comp : components) - { - if(comp.get_name()==component_name) - { - // done - if(bit_field_width!=0) - dest=plus_exprt(dest, from_integer(bit_field_width/8, size_type())); - return dest; - } - - if(comp.get_bool(ID_is_type)) - continue; - - const typet &sub_type=ns.follow(comp.type()); - - if(sub_type.id()==ID_code) - { - } - else if(sub_type.id()==ID_c_bit_field) - { - // We just sum them up. - // This assumes they are properly padded. - bit_field_width+=to_c_bit_field_type(sub_type).get_width(); - } - else - { - exprt tmp=sizeof_rec(sub_type); - - if(tmp.is_nil()) - return tmp; - - exprt sum=plus_exprt(dest, tmp); - dest=sum; - } - } - - return nil_exprt(); -} - -exprt c_sizeof(const typet &src, const namespacet &ns) -{ - c_sizeoft c_sizeof_inst(ns); - exprt tmp=c_sizeof_inst(src); - simplify(tmp, ns); - return tmp; -} - -exprt c_offsetof( - const struct_typet &src, - const irep_idt &component_name, - const namespacet &ns) -{ - c_sizeoft c_sizeof_inst(ns); - exprt tmp=c_sizeof_inst.c_offsetof(src, component_name); - simplify(tmp, ns); - return tmp; -} diff --git a/src/ansi-c/c_sizeof.h b/src/ansi-c/c_sizeof.h deleted file mode 100644 index de5421c0510..00000000000 --- a/src/ansi-c/c_sizeof.h +++ /dev/null @@ -1,51 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_ANSI_C_C_SIZEOF_H -#define CPROVER_ANSI_C_C_SIZEOF_H - -#include -#include - -class c_sizeoft -{ -public: - explicit c_sizeoft(const namespacet &_ns):ns(_ns) - { - } - - virtual ~c_sizeoft() - { - } - - exprt operator()(const typet &type) - { - return sizeof_rec(type); - } - - exprt c_offsetof( - const struct_typet &type, - const irep_idt &component_name); - -protected: - const namespacet &ns; - - virtual exprt sizeof_rec(const typet &type); -}; - -exprt c_sizeof( - const typet &src, - const namespacet &ns); - -exprt c_offsetof( - const struct_typet &src, - const irep_idt &component_name, - const namespacet &ns); - -#endif // CPROVER_ANSI_C_C_SIZEOF_H diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 54eab363d7b..746e03be6d3 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -26,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "c_typecast.h" -#include "c_sizeof.h" #include "c_qualifiers.h" #include "string_constant.h" #include "anonymous_member.h" @@ -556,7 +555,9 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) if(type.id()==ID_struct) { - exprt o=c_offsetof(to_struct_type(type), component_name, *this); + exprt o= + member_offset_expr( + to_struct_type(type), component_name, *this); if(o.is_nil()) { @@ -597,7 +598,8 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) if(type.id()==ID_struct) { exprt o= - c_offsetof(to_struct_type(type), c_it->get_name(), *this); + member_offset_expr( + to_struct_type(type), c_it->get_name(), *this); if(o.is_nil()) { @@ -649,7 +651,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) // still need to typecheck index typecheck_expr(index); - exprt sub_size=c_sizeof(type.subtype(), *this); + exprt sub_size=size_of_expr(type.subtype(), *this); if(index.type()!=size_type()) index.make_typecast(size_type()); result=plus_exprt(result, mult_exprt(sub_size, index)); @@ -946,7 +948,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr) throw 0; } - exprt new_expr=c_sizeof(type, *this); + exprt new_expr=size_of_expr(type, *this); if(new_expr.is_nil()) { diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 1a3998de19d..1a6bf27adad 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "c_sizeof.h" #include "c_qualifiers.h" #include "ansi_c_declaration.h" #include "padding.h" @@ -661,7 +660,7 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type) } // the subtype must have constant size - exprt size_expr=c_sizeof(type.subtype(), *this); + exprt size_expr=size_of_expr(type.subtype(), *this); simplify(size_expr, *this); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index cac26bd5dc3..dec8510eb7b 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include +#include #include #include #include @@ -22,7 +23,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include @@ -856,8 +856,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) // runtime library exprt &sizeof_expr=static_cast(expr.add(ID_sizeof)); - sizeof_expr=c_sizeof(expr.type().subtype(), *this); - sizeof_expr.add("#c_sizeof_type")=expr.type().subtype(); + sizeof_expr=size_of_expr(expr.type().subtype(), *this); + sizeof_expr.add(ID_C_c_sizeof_type)=expr.type().subtype(); } static exprt collect_comma_expression(const exprt &src) diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 7795b71e4c0..013f861886d 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -12,11 +12,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck.h" #include +#include +#include #include #include -#include -#include #include "cpp_util.h" @@ -228,8 +228,6 @@ void cpp_typecheckt::zero_initializer( } else if(final_type.id()==ID_union) { - c_sizeoft c_sizeof(*this); - // Select the largest component for zero-initialization mp_integer max_comp_size=0; @@ -244,7 +242,7 @@ void cpp_typecheckt::zero_initializer( if(component.type().id()==ID_code) continue; - exprt component_size=c_sizeof(component.type()); + exprt component_size=size_of_expr(component.type(), *this); mp_integer size_int; if(!to_integer(component_size, size_int)) diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 2897a4e6697..df319f3deb5 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -13,6 +13,7 @@ Date: November 2011 #include "stack_depth.h" +#include #include #include #include diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 798266792eb..e5e3dea6796 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -211,14 +211,11 @@ mp_integer pointer_offset_bits( type.id()==ID_fixedbv || type.id()==ID_floatbv || type.id()==ID_bv || - type.id()==ID_c_bool) + type.id()==ID_c_bool || + type.id()==ID_c_bit_field) { return to_bitvector_type(type).get_width(); } - else if(type.id()==ID_c_bit_field) - { - return to_c_bit_field_type(type).get_width(); - } else if(type.id()==ID_c_enum) { return to_bitvector_type(type.subtype()).get_width(); @@ -233,6 +230,10 @@ mp_integer pointer_offset_bits( } else if(type.id()==ID_pointer) { + // the following is an MS extension + if(type.get_bool(ID_C_ptr32)) + return 32; + return config.ansi_c.pointer_width; } else if(type.id()==ID_symbol) @@ -248,7 +249,7 @@ mp_integer pointer_offset_bits( return 32; } else - return mp_integer(-1); + return -1; } exprt member_offset_expr( @@ -408,7 +409,8 @@ exprt size_of_expr( const union_typet::componentst &components= union_type.components(); - mp_integer result=0; + mp_integer max_bytes=0; + exprt result=from_integer(0, size_type()); // compute max @@ -418,35 +420,52 @@ exprt size_of_expr( it++) { const typet &subtype=it->type(); - mp_integer sub_size; + exprt sub_size; - if(subtype.id()==ID_c_bit_field) + mp_integer sub_bits=pointer_offset_bits(subtype, ns); + + if(sub_bits==-1) { - std::size_t bits=to_c_bit_field_type(subtype).get_width(); - sub_size=bits/8; - if((bits%8)!=0) - ++sub_size; + max_bytes=-1; + + sub_size=size_of_expr(subtype, ns); + if(sub_size.is_nil()) + return nil_exprt(); } else - sub_size=pointer_offset_size(subtype, ns); - - if(sub_size==-1) { - result=-1; - break; + mp_integer sub_bytes=(sub_bits+7)/8; + + if(max_bytes>=0) + { + if(max_bytesresult) - result=sub_size; + + result=if_exprt( + binary_relation_exprt(result, ID_lt, sub_size), + sub_size, result); + + simplify(result, ns); } - return from_integer(result, size_type()); + return result; } else if(type.id()==ID_signedbv || type.id()==ID_unsignedbv || type.id()==ID_fixedbv || type.id()==ID_floatbv || type.id()==ID_bv || - type.id()==ID_c_bool) + type.id()==ID_c_bool || + type.id()==ID_c_bit_field) { std::size_t width=to_bitvector_type(type).get_width(); std::size_t bytes=width/8; @@ -472,6 +491,10 @@ exprt size_of_expr( } else if(type.id()==ID_pointer) { + // the following is an MS extension + if(type.get_bool(ID_C_ptr32)) + return from_integer(4, size_type()); + std::size_t width=config.ansi_c.pointer_width; std::size_t bytes=width/8; if(bytes*8!=width) From 1fa569fd17ca8b7512d830211ebf985dc7861336 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 7 Aug 2017 14:38:57 +0000 Subject: [PATCH 2/4] sizeof(*(void*)) is sizeof(char) --- regression/ansi-c/sizeof5/main.c | 15 +++++++++++++++ regression/ansi-c/sizeof5/test.desc | 8 ++++++++ src/ansi-c/c_typecheck_expr.cpp | 6 ++++++ 3 files changed, 29 insertions(+) create mode 100644 regression/ansi-c/sizeof5/main.c create mode 100644 regression/ansi-c/sizeof5/test.desc diff --git a/regression/ansi-c/sizeof5/main.c b/regression/ansi-c/sizeof5/main.c new file mode 100644 index 00000000000..7149902ced6 --- /dev/null +++ b/regression/ansi-c/sizeof5/main.c @@ -0,0 +1,15 @@ +#define STATIC_ASSERT(condition) \ + int some_array##__LINE__[(condition) ? 1 : -1]; + +struct S +{ + int x; +}; + +int main() +{ + struct S s; + __typeof__(*((void *)&s.x)) *_s=&s.x; + STATIC_ASSERT(sizeof(*_s)==1); + return 0; +} diff --git a/regression/ansi-c/sizeof5/test.desc b/regression/ansi-c/sizeof5/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/sizeof5/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 746e03be6d3..b28156b52a5 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -948,6 +948,12 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr) throw 0; } + if(type.id()==ID_empty && + expr.operands().size()==1 && + expr.op0().id()==ID_dereference && + expr.op0().op0().type()==pointer_type(void_type())) + type=char_type(); + exprt new_expr=size_of_expr(type, *this); if(new_expr.is_nil()) From 3273bf5b97660d7c0a87120f938762f04caa3465 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Aug 2017 16:27:24 +0000 Subject: [PATCH 3/4] Fix type casts from initializer lists to arrays of unspecified size --- regression/ansi-c/Initializer_cast2/main.c | 6 ++++++ regression/ansi-c/Initializer_cast2/test.desc | 7 +++++++ src/ansi-c/c_typecheck_expr.cpp | 9 ++++++++- 3 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 regression/ansi-c/Initializer_cast2/main.c create mode 100644 regression/ansi-c/Initializer_cast2/test.desc diff --git a/regression/ansi-c/Initializer_cast2/main.c b/regression/ansi-c/Initializer_cast2/main.c new file mode 100644 index 00000000000..710bbdc0683 --- /dev/null +++ b/regression/ansi-c/Initializer_cast2/main.c @@ -0,0 +1,6 @@ +int main() +{ + int A[(sizeof((int[]){1, 2, 3})==3*sizeof(int))?1:-1]; + + return 0; +} diff --git a/regression/ansi-c/Initializer_cast2/test.desc b/regression/ansi-c/Initializer_cast2/test.desc new file mode 100644 index 00000000000..854d67addcf --- /dev/null +++ b/regression/ansi-c/Initializer_cast2/test.desc @@ -0,0 +1,7 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^CONVERSION ERROR$ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b28156b52a5..e45dc1a4d89 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1100,7 +1100,14 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr) // or an expression for a pointer or scalar. // We produce a compound_literal expression. exprt tmp(ID_compound_literal, expr.type()); - tmp.move_to_operands(op); + tmp.copy_to_operands(op); + + // handle the case of TYPE being an array with unspecified size + if(op.id()==ID_array && + expr.type().id()==ID_array && + to_array_type(expr.type()).size().is_nil()) + tmp.type()=op.type(); + expr=tmp; expr.set(ID_C_lvalue, true); // these are l-values return; From 3613ebca0a4197fb51f076277f41696e46e6036e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Aug 2017 15:51:18 +0000 Subject: [PATCH 4/4] When possible, update array types before typechecking initializer This fixes a bug in compiling a Linux kernel driver. --- .../ansi-c/array_initialization3/main.c | 13 +++++ .../ansi-c/array_initialization3/test.desc | 8 ++++ src/ansi-c/c_typecheck_base.cpp | 47 +++++++------------ 3 files changed, 39 insertions(+), 29 deletions(-) create mode 100644 regression/ansi-c/array_initialization3/main.c create mode 100644 regression/ansi-c/array_initialization3/test.desc diff --git a/regression/ansi-c/array_initialization3/main.c b/regression/ansi-c/array_initialization3/main.c new file mode 100644 index 00000000000..6e7fb047488 --- /dev/null +++ b/regression/ansi-c/array_initialization3/main.c @@ -0,0 +1,13 @@ +#define STATIC_ASSERT_sizeof(condition) \ + int[(condition) ? 1 : -1] + +int A[]; +int B[]; + +int A[1]={sizeof(A)}; +int B[1]={sizeof(STATIC_ASSERT_sizeof(sizeof(B)==sizeof(int)))}; + +int main() +{ + return 0; +} diff --git a/regression/ansi-c/array_initialization3/test.desc b/regression/ansi-c/array_initialization3/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/array_initialization3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 0d18016602d..b0a8f1734c3 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_typecheck_base.h" +#include #include #include #include @@ -256,6 +257,16 @@ void c_typecheck_baset::typecheck_redefinition_non_type( // this is ok, just use old type new_symbol.type=old_symbol.type; } + else if(final_old.id()==ID_array && + to_array_type(final_old).size().is_nil() && + initial_new.id()==ID_array && + to_array_type(initial_new).size().is_not_nil() && + final_old.subtype()==initial_new.subtype()) + { + // update the type to enable the use of sizeof(x) on the + // right-hand side of a definition of x + old_symbol.type=new_symbol.type; + } // do initializer, this may change the type if(follow(new_symbol.type).id()!=ID_code && @@ -386,36 +397,14 @@ void c_typecheck_baset::typecheck_redefinition_non_type( if(final_old!=final_new) { if(final_old.id()==ID_array && - to_array_type(final_old).size().is_nil() && - final_new.id()==ID_array && - to_array_type(final_new).size().is_not_nil() && - final_old.subtype()==final_new.subtype()) + to_array_type(final_old).size().is_nil() && + final_new.id()==ID_array && + to_array_type(final_new).size().is_not_nil() && + final_old.subtype()==final_new.subtype()) { - // this is also ok - if(old_symbol.type.id()==ID_symbol) - { - // fix the symbol, not just the type - const irep_idt identifier= - to_symbol_type(old_symbol.type).get_identifier(); - - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(identifier); - - if(s_it==symbol_table.symbols.end()) - { - error().source_location=old_symbol.location; - error() << "typecheck_redefinition_non_type: " - << "failed to find symbol `" << identifier << "'" - << eom; - throw 0; - } - - symbolt &symbol=s_it->second; - - symbol.type=final_new; - } - else - old_symbol.type=new_symbol.type; + // we don't do symbol types for arrays anymore + PRECONDITION(old_symbol.type.id()!=ID_symbol); + old_symbol.type=new_symbol.type; } else if((final_old.id()==ID_incomplete_c_enum || final_old.id()==ID_c_enum) &&