Skip to content

Commit 00f95f8

Browse files
committed
C front-end: address-of-label is a compile-time constant
When using computed gotos, the addresses of labels are taken. These are compile-time constants that are safe to use in initializers of objects with static lifetime.
1 parent f02532a commit 00f95f8

File tree

2 files changed

+3
-1
lines changed

2 files changed

+3
-1
lines changed

regression/cbmc/Computed-Goto1/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
int main()
22
{
3-
void *table[]={ &&l0, &&l1, &&l2 };
3+
static void *table[] = {&&l0, &&l1, &&l2};
44
int in, out;
55

66
if(in>=0 && in<=2)

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4520,6 +4520,8 @@ class is_compile_time_constantt : public is_constantt
45204520
}
45214521
else if(e.id() == ID_array && e.get_bool(ID_C_string_constant))
45224522
return true;
4523+
else if(e.id() == ID_label)
4524+
return true;
45234525
else
45244526
return is_constantt::is_constant_address_of(e);
45254527
}

0 commit comments

Comments
 (0)