C23 keywords

README.md

@@ -6,13 +6,14 @@
 About
 =====
 
-CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99,
-most of C11 and most compiler extensions provided by gcc and Visual Studio. It
-also supports SystemC using Scoot. It allows verifying array bounds (buffer
-overflows), pointer safety, exceptions and user-specified assertions.
-Furthermore, it can check C and C++ for consistency with other languages, such
-as Verilog. The verification is performed by unwinding the loops in the program
-and passing the resulting equation to a decision procedure.
+CBMC is a Bounded Model Checker for C and C++ programs.  It supports C89,
+C99, most of C11, C17, C23 and most compiler extensions provided by gcc and
+Visual Studio.  It also supports SystemC using Scoot.  It allows verifying
+array bounds (buffer overflows), pointer safety, exceptions and
+user-specified assertions.  Furthermore, it can check C and C++ for
+consistency with other languages, such as Verilog.  The verification is
+performed by unwinding the loops in the program and passing the resulting
+equation to a decision procedure.
 
 For full information see [cprover.org](http://www.cprover.org/cbmc).
 

doc/architectural/front-page.md

@@ -8,13 +8,14 @@ website</a>; contributors should use the
 <a href="https://github.com/diffblue/cbmc">repository</a> hosted on GitHub. CBMC
 is part of CProver.
 
-CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99,
-most of C11 and most compiler extensions provided by gcc and Visual Studio. It
-also supports SystemC using Scoot. It allows verifying array bounds (buffer
-overflows), pointer safety, arithmetic exceptions and user-specified assertions.
-Furthermore, it can check C and C++ for consistency with other languages, such
-as Verilog. The verification is performed by unwinding the loops in the program
-and passing the resulting equation to a decision procedure.
+CBMC is a Bounded Model Checker for C and C++ programs.  It supports C89,
+C99, most of C11, C17, C23 and most compiler extensions provided by gcc and
+Visual Studio.  It also supports SystemC using Scoot.  It allows verifying
+array bounds (buffer overflows), pointer safety, arithmetic exceptions and
+user-specified assertions.  Furthermore, it can check C and C++ for
+consistency with other languages, such as Verilog.  The verification is
+performed by unwinding the loops in the program and passing the resulting
+equation to a decision procedure.
 
 For further information see [cprover.org](http://www.cprover.org/cbmc).
 

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\-\-c23\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,13 @@
+// _BitInt is a C23 feature
+
+// sizeof
+static_assert(sizeof(unsigned _BitInt(1)) == 1);
+static_assert(sizeof(_BitInt(32)) == 4);
+static_assert(sizeof(_BitInt(33)) == 8);
+static_assert(sizeof(_BitInt(65)) == 16);
+static_assert(sizeof(_BitInt(128)) == 16);
+
+int main()
+{
+  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/_BitInt/_BitInt2.c

@@ -0,0 +1,18 @@
+// _BitInt is a C23 feature
+#include <assert.h>
+
+int main()
+{
+  // 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);
+
+  return 0;
+}

regression/cbmc/_BitInt/_BitInt2.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+_BitInt2.c
+--c23
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+_BitInt implementation is missing.

regression/cbmc/_BitInt/_BitInt3.c

@@ -0,0 +1,11 @@
+// _BitInt is a C23 feature
+#include <assert.h>
+
+int main()
+{
+  // pointers
+  _BitInt(3) x, *p = &x;
+  *p = 1;
+
+  return 0;
+}

regression/cbmc/_BitInt/_BitInt3.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+_BitInt3.c
+--c23
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+_BitInt implementation is missing.

regression/cbmc/_BitInt/_BitInt4.c

@@ -0,0 +1,10 @@
+// _BitInt is a C23 feature
+
+static_assert(6uwb + -6wb == 0);
+static_assert(sizeof(255uwb + 1uwb) == 1);
+static_assert(sizeof(0b1111'1111uwb) == 1);
+
+int main()
+{
+  return 0;
+}

regression/cbmc/_BitInt/_BitInt4.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+_BitInt4.c
+--c23
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+_BitInt implementation is missing.

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$

src/ansi-c/ansi_c_convert_type.cpp

@@ -77,6 +77,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     int32_cnt++;
   else if(type.id()==ID_int64)
     int64_cnt++;
+  else if(type.id() == ID_c_bitint)
+  {
+    bitint_cnt++;
+    const exprt &size_expr = static_cast<const exprt &>(type.find(ID_size));
+
+    bv_width = size_expr;
+  }
   else if(type.id()==ID_gcc_float16)
     gcc_float16_cnt++;
   else if(type.id()==ID_gcc_float32)
@@ -290,15 +297,13 @@ void ansi_c_convert_typet::write(typet &type)
 
   if(!other.empty())
   {
-    if(double_cnt || float_cnt || signed_cnt ||
-       unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
-       short_cnt || char_cnt || complex_cnt || long_cnt ||
-       int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
-       gcc_float16_cnt ||
-       gcc_float32_cnt || gcc_float32x_cnt ||
-       gcc_float64_cnt || gcc_float64x_cnt ||
-       gcc_float128_cnt || gcc_float128x_cnt ||
-       gcc_int128_cnt || bv_cnt)
+    if(
+      double_cnt || float_cnt || signed_cnt || unsigned_cnt || int_cnt ||
+      c_bool_cnt || proper_bool_cnt || bitint_cnt || short_cnt || char_cnt ||
+      complex_cnt || long_cnt || int8_cnt || int16_cnt || int32_cnt ||
+      int64_cnt || gcc_float16_cnt || gcc_float32_cnt || gcc_float32x_cnt ||
+      gcc_float64_cnt || gcc_float64x_cnt || gcc_float128_cnt ||
+      gcc_float128x_cnt || gcc_int128_cnt || bv_cnt)
     {
       log.error().source_location = source_location;
       log.error() << "illegal type modifier for defined type" << messaget::eom;
@@ -373,10 +378,10 @@ void ansi_c_convert_typet::write(typet &type)
           gcc_float64_cnt || gcc_float64x_cnt ||
           gcc_float128_cnt || gcc_float128x_cnt)
   {
-    if(signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
-       int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
-       gcc_int128_cnt || bv_cnt ||
-       short_cnt || char_cnt)
+    if(
+      signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
+      bitint_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
+      gcc_int128_cnt || bv_cnt || short_cnt || char_cnt)
     {
       log.error().source_location = source_location;
       log.error() << "cannot combine integer type with floating-point type"
@@ -415,10 +420,10 @@ void ansi_c_convert_typet::write(typet &type)
   }
   else if(double_cnt || float_cnt)
   {
-    if(signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
-       int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
-       gcc_int128_cnt|| bv_cnt ||
-       short_cnt || char_cnt)
+    if(
+      signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
+      bitint_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
+      gcc_int128_cnt || bv_cnt || short_cnt || char_cnt)
     {
       log.error().source_location = source_location;
       log.error() << "cannot combine integer type with floating-point type"
@@ -460,10 +465,10 @@ void ansi_c_convert_typet::write(typet &type)
   }
   else if(c_bool_cnt)
   {
-    if(signed_cnt || unsigned_cnt || int_cnt || short_cnt ||
-       int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
-       gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
-       char_cnt || long_cnt)
+    if(
+      signed_cnt || unsigned_cnt || int_cnt || short_cnt || bitint_cnt ||
+      int8_cnt || int16_cnt || int32_cnt || int64_cnt || gcc_float128_cnt ||
+      bv_cnt || proper_bool_cnt || char_cnt || long_cnt)
     {
       log.error().source_location = source_location;
       log.error() << "illegal type modifier for C boolean type"
@@ -475,10 +480,10 @@ void ansi_c_convert_typet::write(typet &type)
   }
   else if(proper_bool_cnt)
   {
-    if(signed_cnt || unsigned_cnt || int_cnt || short_cnt ||
-       int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
-       gcc_float128_cnt || bv_cnt ||
-       char_cnt || long_cnt)
+    if(
+      signed_cnt || unsigned_cnt || int_cnt || short_cnt || bitint_cnt ||
+      int8_cnt || int16_cnt || int32_cnt || int64_cnt || gcc_float128_cnt ||
+      bv_cnt || char_cnt || long_cnt)
     {
       log.error().source_location = source_location;
       log.error() << "illegal type modifier for proper boolean type"
@@ -496,9 +501,9 @@ void ansi_c_convert_typet::write(typet &type)
   }
   else if(char_cnt)
   {
-    if(int_cnt || short_cnt || long_cnt ||
-       int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
-       gcc_float128_cnt || bv_cnt || proper_bool_cnt)
+    if(
+      int_cnt || short_cnt || long_cnt || bitint_cnt || int8_cnt || int16_cnt ||
+      int32_cnt || int64_cnt || gcc_float128_cnt || bv_cnt || proper_bool_cnt)
     {
       log.error().source_location = source_location;
       log.error() << "illegal type modifier for char type" << messaget::eom;
@@ -537,7 +542,9 @@ void ansi_c_convert_typet::write(typet &type)
 
     if(int8_cnt || int16_cnt || int32_cnt || int64_cnt)
     {
-      if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
+      if(
+        long_cnt || char_cnt || short_cnt || bitint_cnt || gcc_int128_cnt ||
+        bv_cnt)
       {
         log.error().source_location = source_location;
         log.error() << "conflicting type modifiers" << messaget::eom;
@@ -574,6 +581,12 @@ void ansi_c_convert_typet::write(typet &type)
       else
         type=gcc_unsigned_int128_type();
     }
+    else if(bitint_cnt)
+    {
+      // explicitly-given expression for the number of value bits
+      type.id(is_signed ? ID_c_signed_bitint : ID_c_unsigned_bitint);
+      type.set(ID_width, bv_width);
+    }
     else if(bv_cnt)
     {
       // explicitly-given expression for width

src/ansi-c/ansi_c_convert_type.h

@@ -24,10 +24,8 @@ class message_handlert;
 class ansi_c_convert_typet
 {
 public:
-  unsigned unsigned_cnt, signed_cnt, char_cnt,
-           int_cnt, short_cnt, long_cnt,
-           double_cnt, float_cnt, c_bool_cnt,
-           proper_bool_cnt, complex_cnt;
+  unsigned unsigned_cnt, signed_cnt, char_cnt, int_cnt, short_cnt, long_cnt,
+    double_cnt, float_cnt, c_bool_cnt, proper_bool_cnt, complex_cnt, bitint_cnt;
 
   // extensions
   unsigned int8_cnt, int16_cnt, int32_cnt, int64_cnt,
@@ -87,6 +85,7 @@ class ansi_c_convert_typet
       c_bool_cnt(0),
       proper_bool_cnt(0),
       complex_cnt(0),
+      bitint_cnt(0),
       int8_cnt(0),
       int16_cnt(0),
       int32_cnt(0),