Skip to content

Commit 59ff926

Browse files
authored
Merge pull request #6663 from tautschnig/feature/annotate-flexible-array
Annotate flexible array members
2 parents 43b0ac8 + 24eba85 commit 59ff926

File tree

5 files changed

+15
-4
lines changed

5 files changed

+15
-4
lines changed

src/analyses/goto_check_c.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1621,15 +1621,17 @@ void goto_check_ct::bounds_check_index(
16211621
? to_array_type(array_type).size()
16221622
: to_vector_type(array_type).size();
16231623

1624-
if(size.is_nil())
1624+
if(size.is_nil() && !array_type.get_bool(ID_C_flexible_array_member))
16251625
{
16261626
// Linking didn't complete, we don't have a size.
16271627
// Not clear what to do.
16281628
}
16291629
else if(size.id() == ID_infinity)
16301630
{
16311631
}
1632-
else if(size.is_zero() && expr.array().id() == ID_member)
1632+
else if(
1633+
expr.array().id() == ID_member &&
1634+
(size.is_zero() || array_type.get_bool(ID_C_flexible_array_member)))
16331635
{
16341636
// a variable sized struct member
16351637
//

src/ansi-c/c_typecheck_type.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1010,8 +1010,8 @@ void c_typecheck_baset::typecheck_compound_body(
10101010
}
10111011

10121012
// make it zero-length
1013-
c_type.id(ID_array);
1014-
c_type.set(ID_size, from_integer(0, c_index_type()));
1013+
to_array_type(c_type).size() = from_integer(0, c_index_type());
1014+
c_type.set(ID_C_flexible_array_member, true);
10151015
}
10161016
}
10171017
}

src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -868,6 +868,7 @@ IREP_ID_ONE(bitreverse)
868868
IREP_ID_ONE(saturating_minus)
869869
IREP_ID_ONE(saturating_plus)
870870
IREP_ID_ONE(annotated_pointer_constant)
871+
IREP_ID_TWO(C_flexible_array_member, #flexible_array_member)
871872

872873
// Projects depending on this code base that wish to extend the list of
873874
// available ids should provide a file local_irep_ids.def in their source tree

src/util/pointer_offset_size.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -368,6 +368,11 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
368368
if(bytes > 0)
369369
result = plus_exprt(result, from_integer(bytes, result.type()));
370370
}
371+
else if(c.type().get_bool(ID_C_flexible_array_member))
372+
{
373+
// flexible array members do not change the sizeof result
374+
continue;
375+
}
371376
else
372377
{
373378
DATA_INVARIANT(

src/util/simplify_expr.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1746,6 +1746,9 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
17461746
if(comps.empty() || comps.back().type().id() != ID_array)
17471747
return false;
17481748

1749+
if(comps.back().type().get_bool(ID_C_flexible_array_member))
1750+
return true;
1751+
17491752
const auto size =
17501753
numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
17511754
return !size.has_value() || *size <= 1;

0 commit comments

Comments
 (0)