Fix #779: Mark offset off as an integer constant

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
 

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");

tests/cn/offsetof_int_const.c.verify

@@ -0,0 +1 @@
+return code: 0

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