diff --git a/frontend/model/cabs_to_ail.lem b/frontend/model/cabs_to_ail.lem index 8907f3cdf..7cf36c554 100644 --- a/frontend/model/cabs_to_ail.lem +++ b/frontend/model/cabs_to_ail.lem @@ -601,7 +601,8 @@ let rec is_integer_constant_expression (AnnotatedExpression () _ loc expr_ as ex | AilEassert _ -> E.return false | AilEoffsetof _ _ -> - E.fail loc (Errors.Desugar_NotYetSupported "offsetof() in `integer constant expressions'") + (* STD §7.19#3 *) + E.return true | AilEstr _ -> E.return false (* @@ -833,7 +834,9 @@ let rec is_arithmetic_constant_expression is_lvalue ((AnnotatedExpression () _ l (* E.return true *) (* TODO: is_lvalue might be wrong depending on the type of e? *) is_arithmetic_constant_expression is_lvalue e - + | AilEoffsetof _ _ -> + (* STD §7.19#3 *) + E.return true | _ -> E.return false diff --git a/tests/cn/offsetof_int_const.c b/tests/cn/offsetof_int_const.c new file mode 100644 index 000000000..24df04c7b --- /dev/null +++ b/tests/cn/offsetof_int_const.c @@ -0,0 +1,5 @@ +typedef struct a { + int b; + int c; +} a; +_Static_assert(offsetof(a, c) == sizeof(int), "no gap"); diff --git a/tests/cn/offsetof_int_const.c.verify b/tests/cn/offsetof_int_const.c.verify new file mode 100644 index 000000000..e1522bb41 --- /dev/null +++ b/tests/cn/offsetof_int_const.c.verify @@ -0,0 +1 @@ +return code: 0 diff --git a/tests/run-cn-exec.sh b/tests/run-cn-exec.sh index 14ca26277..1f7319fd6 100755 --- a/tests/run-cn-exec.sh +++ b/tests/run-cn-exec.sh @@ -102,6 +102,7 @@ SUCCESS=$(find cn -name '*.c' \ ! -name "int_to_ptr.c" \ ! -name "int_to_ptr.error.c" \ ! -name "create_rdonly.c" \ + ! -name "offsetof_int_const.c" \ ) # Include files which cause error for proof but not testing @@ -168,6 +169,7 @@ BUGGY="cn/division_casting.c \ cn/int_to_ptr.c \ cn/int_to_ptr.error.c \ cn/create_rdonly.c \ + cn/offsetof_int_const.c \ " # Exclude files which cause error for proof but not testing