Skip to content

Commit

Permalink
Do not use nil_typet in c_bit_field_replacement_type
Browse files Browse the repository at this point in the history
No caller handles that case, instead insert appropriate PRECONDITIONs.
  • Loading branch information
tautschnig committed Jan 26, 2019
1 parent 85d61b5 commit 83682da
Showing 1 changed file with 11 additions and 13 deletions.
24 changes: 11 additions & 13 deletions src/solvers/flattening/c_bit_field_replacement_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,10 @@ Author: Daniel Kroening, [email protected]
\*******************************************************************/


#include "c_bit_field_replacement_type.h"

#include <util/invariant.h>

typet c_bit_field_replacement_type(
const c_bit_field_typet &src,
const namespacet &ns)
Expand All @@ -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();
}

0 comments on commit 83682da

Please sign in to comment.