C23 keywords

This adds scanner, parser and typechecker support for the new C23 keywords.

Author: kroening

doc/man/cbmc.1

@@ -154,7 +154,7 @@ set include file (C/C++)
 \fB\-D\fR macro
 define preprocessor macro (C/C++)
 .TP
-\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR
+\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR, \fB\-\-c17\fR, \fB\-\-c23\fR
 set C language standard (default: c11)
 .TP
 \fB\-\-cpp98\fR, \fB\-\-cpp03\fR, \fB\-\-cpp11\fR

doc/man/goto-analyzer.1

@@ -425,7 +425,7 @@ set include file (C/C++)
 \fB\-D\fR macro
 define preprocessor macro (C/C++)
 .TP
-\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR
+\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR, \fB\-\-c17\fR, \fB\-\-c21\fR
 set C language standard (default: c11)
 .TP
 \fB\-\-cpp98\fR, \fB\-\-cpp03\fR, \fB\-\-cpp11\fR

regression/cbmc/_BitInt/_BitInt1.c

@@ -0,0 +1,28 @@
+// _BitInt is a C23 feature
+#include <assert.h>
+
+int main()
+{
+  // sizeof
+  static_assert(sizeof(_BitInt(32)) == 4);
+  static_assert(sizeof(_BitInt(33)) == 8);
+  static_assert(sizeof(_BitInt(65)) == 16);
+  static_assert(sizeof(_BitInt(128)) == 16);
+
+  // casts
+  //assert((_BitInt(4))17 == 1);
+  //assert((_BitInt(4)) - 1 == -1);
+  //assert((unsigned _BitInt(4)) - 1 == 15);
+
+  // promotion (or lack thereof)
+  //assert((unsigned _BitInt(4))15 + (unsigned _BitInt(4))1 == 0);
+  // assert((unsigned _BitInt(4))15 + (unsigned _BitInt(5))1 == 16);
+  //assert((unsigned _BitInt(4))15 + (signed _BitInt(5))1 == -16);
+  // assert((unsigned _BitInt(4))15 + 1 == 16);
+
+  // pointers
+  _BitInt(3) x, *p = &x;
+  //*p = 1;
+
+  return 0;
+}

regression/cbmc/_BitInt/_BitInt1.desc

@@ -0,0 +1,8 @@
+CORE
+_BitInt1.c
+--c23
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc/constants/predefined-constants1.c

@@ -0,0 +1,10 @@
+// C23 predefined constants
+static_assert(!false, "false");
+static_assert(true, "true");
+static_assert(sizeof(false) == sizeof(bool), "sizeof false");
+static_assert(sizeof(true) == sizeof(bool), "sizeof true");
+static_assert(nullptr == 0, "nullptr");
+
+int main()
+{
+}

regression/cbmc/constants/predefined-constants1.desc

@@ -0,0 +1,7 @@
+CORE
+predefined-constants1.c
+--c23
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/static_assert/static_assert1.c

@@ -0,0 +1,17 @@
+// C23 introduces the "static_assert" keyword.
+
+struct S
+{
+  // Visual Studio does not support static_assert in compound bodies.
+#ifndef _MSC_VER
+  static_assert(1, "in struct");
+#endif
+  int x;
+} asd;
+
+static_assert(1, "global scope");
+
+int main()
+{
+  static_assert(1, "in function");
+}

regression/cbmc/static_assert/static_assert1.desc

@@ -0,0 +1,8 @@
+CORE
+static_assert1.c
+--c23
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc/typeof/typeof2.c

@@ -0,0 +1,23 @@
+typedef int INTTYPE;
+
+int func1();
+
+// C23 typeof
+typeof(int) v1;
+typeof(INTTYPE) v2;
+typeof(v2) v3;
+typeof(1 + 1) v4;
+typeof(1 + 1 + func1()) v5;
+const typeof(int) v6;
+typeof(int) const v7;
+static typeof(int) const v8;
+static typeof(int) const *v9;
+static volatile typeof(int) const *v10;
+
+void func2(typeof(int) *some_arg)
+{
+}
+
+int main()
+{
+}

regression/cbmc/typeof/typeof2.desc

@@ -0,0 +1,8 @@
+CORE
+typeof2.c
+--c23
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$