File tree 2 files changed +9
-2
lines changed
regression/cbmc/assigning_nullpointers_should_not_crash_symex
2 files changed +9
-2
lines changed Original file line number Diff line number Diff line change 1
- KNOWNBUG
1
+ CORE
2
2
main.c
3
3
4
4
^EXIT=0$
Original file line number Diff line number Diff line change @@ -1740,7 +1740,7 @@ optionalt<std::string> simplify_exprt::expr2bits(
1740
1740
if (
1741
1741
type.id () == ID_unsignedbv || type.id () == ID_signedbv ||
1742
1742
type.id () == ID_floatbv || type.id () == ID_fixedbv ||
1743
- type.id () == ID_c_bit_field || type. id () == ID_pointer )
1743
+ type.id () == ID_c_bit_field)
1744
1744
{
1745
1745
const auto width = to_bitvector_type (type).get_width ();
1746
1746
@@ -1753,6 +1753,13 @@ optionalt<std::string> simplify_exprt::expr2bits(
1753
1753
1754
1754
return result;
1755
1755
}
1756
+ else if (type.id () == ID_pointer)
1757
+ {
1758
+ if (value == ID_NULL)
1759
+ return std::string (' 0' , to_bitvector_type (type).get_width ());
1760
+ else
1761
+ return {};
1762
+ }
1756
1763
else if (type.id () == ID_c_enum_tag)
1757
1764
{
1758
1765
const auto &c_enum_type = ns.follow_tag (to_c_enum_tag_type (type));
You can’t perform that action at this time.
0 commit comments