File tree 9 files changed +92
-0
lines changed
regression/cbmc/incomplete-sizeof
9 files changed +92
-0
lines changed Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+ #include <stdlib.h>
3
+
4
+ int arr [];
5
+
6
+ int main (int argc , char * * argv )
7
+ {
8
+ size_t s = sizeof (arr );
9
+ assert (s == 4 );
10
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ array.c
3
+
4
+ ^EXIT=6$
5
+ ^SIGNAL=0$
6
+ ^file array.c line \d+ function main: invalid application of \'sizeof\' to an incomplete type$
7
+ ^CONVERSION ERROR$
8
+ --
9
+ ^warning: ignoring
Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+ #include <stdlib.h>
3
+
4
+ enum foo ;
5
+
6
+ int main (int argc , char * * argv )
7
+ {
8
+ size_t s = sizeof (enum foo );
9
+ assert (s == 0 );
10
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ enum.c
3
+
4
+ ^EXIT=6$
5
+ ^SIGNAL=0$
6
+ ^file enum.c line \d+ function main: invalid application of \'sizeof\' to an incomplete type$
7
+ ^CONVERSION ERROR$
8
+ --
9
+ ^warning: ignoring
Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+ #include <stdlib.h>
3
+
4
+ struct foo ;
5
+
6
+ int main (int argc , char * * argv )
7
+ {
8
+ struct foo * thefoo = malloc (sizeof (struct foo ));
9
+ size_t s = sizeof (struct foo );
10
+ assert (s == 0 );
11
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ struct.c
3
+
4
+ ^EXIT=6$
5
+ ^SIGNAL=0$
6
+ ^file struct.c line \d+ function main: invalid application of \'sizeof\' to an incomplete type$
7
+ ^CONVERSION ERROR$
8
+ --
9
+ ^warning: ignoring
Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+ #include <stdlib.h>
3
+
4
+ union foo ;
5
+
6
+ int main (int argc , char * * argv )
7
+ {
8
+ size_t s = sizeof (union foo );
9
+ assert (s == 0 );
10
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ union.c
3
+
4
+ ^EXIT=6$
5
+ ^SIGNAL=0$
6
+ ^file union.c line \d+ function main: invalid application of \'sizeof\' to an incomplete type$
7
+ ^CONVERSION ERROR$
8
+ --
9
+ ^warning: ignoring
Original file line number Diff line number Diff line change @@ -951,6 +951,21 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
951
951
}
952
952
else
953
953
{
954
+ if (
955
+ (type.id () == ID_struct_tag &&
956
+ follow_tag (to_struct_tag_type (type)).is_incomplete ()) ||
957
+ (type.id () == ID_union_tag &&
958
+ follow_tag (to_union_tag_type (type)).is_incomplete ()) ||
959
+ (type.id () == ID_c_enum_tag &&
960
+ follow_tag (to_c_enum_tag_type (type)).is_incomplete ()) ||
961
+ (type.id () == ID_array && to_array_type (type).is_incomplete ()))
962
+ {
963
+ error ().source_location = expr.source_location ();
964
+ error () << " invalid application of \' sizeof\' to an incomplete type\n\t\' "
965
+ << to_string (type) << " \' " << eom;
966
+ throw 0 ;
967
+ }
968
+
954
969
auto size_of_opt = size_of_expr (type, *this );
955
970
956
971
if (!size_of_opt.has_value ())
You can’t perform that action at this time.
0 commit comments