Skip to content

Commit 5cd2d1b

Browse files
authored
Merge pull request #7648 from tautschnig/features/preserve-sizeof
Simplify overflow-result: preserve sizeof annotation
2 parents d2d7f76 + fe89774 commit 5cd2d1b

File tree

3 files changed

+33
-5
lines changed

3 files changed

+33
-5
lines changed

regression/cbmc-library/calloc-01/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
int main()
55
{
6-
int *x = calloc(sizeof(int), 1);
6+
int *x = calloc(sizeof(int), 2);
77
assert(*x == 0);
88
return 0;
99
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--program-only
4+
dynamic_object#1 == \{ 0, 0 \}
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
dynamic_object#1 == \{ 0, (0, )+0 \}
10+
--
11+
calloc with a sizeof argument (over a type larger than a byte) should not result
12+
in a byte array being generated by symex.

src/util/simplify_expr.cpp

Lines changed: 20 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2645,6 +2645,19 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
26452645
if(!expr.op0().is_constant() || !expr.op1().is_constant())
26462646
return unchanged(expr);
26472647

2648+
// preserve the sizeof type annotation
2649+
optionalt<typet> c_sizeof_type;
2650+
for(const auto &op : expr.operands())
2651+
{
2652+
const typet &sizeof_type =
2653+
static_cast<const typet &>(op.find(ID_C_c_sizeof_type));
2654+
if(sizeof_type.is_not_nil())
2655+
{
2656+
c_sizeof_type = sizeof_type;
2657+
break;
2658+
}
2659+
}
2660+
26482661
const auto op0_value = numeric_cast<mp_integer>(expr.op0());
26492662
const auto op1_value = numeric_cast<mp_integer>(expr.op1());
26502663
if(!op0_value.has_value() || !op1_value.has_value())
@@ -2662,21 +2675,24 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
26622675
else
26632676
UNREACHABLE;
26642677

2678+
exprt no_overflow_result_expr =
2679+
from_integer(no_overflow_result, expr.op0().type());
2680+
if(c_sizeof_type.has_value())
2681+
no_overflow_result_expr.set(ID_C_c_sizeof_type, *c_sizeof_type);
2682+
26652683
const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
26662684
const integer_bitvector_typet bv_type{op_type_id, width};
26672685
if(
26682686
no_overflow_result < bv_type.smallest() ||
26692687
no_overflow_result > bv_type.largest())
26702688
{
26712689
return struct_exprt{
2672-
{from_integer(no_overflow_result, expr.op0().type()), true_exprt{}},
2673-
expr.type()};
2690+
{std::move(no_overflow_result_expr), true_exprt{}}, expr.type()};
26742691
}
26752692
else
26762693
{
26772694
return struct_exprt{
2678-
{from_integer(no_overflow_result, expr.op0().type()), false_exprt{}},
2679-
expr.type()};
2695+
{std::move(no_overflow_result_expr), false_exprt{}}, expr.type()};
26802696
}
26812697
}
26822698
}

0 commit comments

Comments
 (0)