From 83682da1d72173a9d6645cb41d4e1eaa5ae23d8e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jan 2019 12:35:04 +0000 Subject: [PATCH] Do not use nil_typet in c_bit_field_replacement_type No caller handles that case, instead insert appropriate PRECONDITIONs. --- .../c_bit_field_replacement_type.cpp | 24 +++++++++---------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/solvers/flattening/c_bit_field_replacement_type.cpp b/src/solvers/flattening/c_bit_field_replacement_type.cpp index 8ef691eb112..ad161d2b334 100644 --- a/src/solvers/flattening/c_bit_field_replacement_type.cpp +++ b/src/solvers/flattening/c_bit_field_replacement_type.cpp @@ -6,9 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #include "c_bit_field_replacement_type.h" +#include + typet c_bit_field_replacement_type( const c_bit_field_typet &src, const namespacet &ns) @@ -23,21 +24,18 @@ typet c_bit_field_replacement_type( result.set_width(src.get_width()); return std::move(result); } - else if(subtype.id()==ID_c_enum_tag) + else { + PRECONDITION(subtype.id() == ID_c_enum_tag); + const typet &sub_subtype= ns.follow_tag(to_c_enum_tag_type(subtype)).subtype(); - if(sub_subtype.id()==ID_signedbv || - sub_subtype.id()==ID_unsignedbv) - { - bitvector_typet result=to_bitvector_type(sub_subtype); - result.set_width(src.get_width()); - return std::move(result); - } - else - return nil_typet(); + PRECONDITION( + sub_subtype.id() == ID_signedbv || sub_subtype.id() == ID_unsignedbv); + + bitvector_typet result = to_bitvector_type(sub_subtype); + result.set_width(src.get_width()); + return std::move(result); } - else - return nil_typet(); }