Parse C11 _Noreturn

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6389 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

regression/ansi-c/_Noreturn1/main.c

@@ -0,0 +1,5 @@
+extern _Noreturn void foo();
+
+int main()
+{
+}

regression/ansi-c/_Noreturn1/test.desc

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

src/ansi-c/ansi_c_convert_type.cpp

@@ -225,6 +225,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       }
     }
   }
+  else if(type.id()==ID_noreturn)
+    c_qualifiers.is_noreturn=true;
   else
     other.push_back(type);
 }

src/ansi-c/c_qualifiers.cpp

@@ -43,6 +43,9 @@ std::string c_qualifierst::as_string() const
 
   if(is_ptr64)
     qualifiers+="__ptr64 ";
+
+  if(is_noreturn)
+    qualifiers+="_Noreturn ";
 
   return qualifiers;
 }
@@ -81,6 +84,9 @@ void c_qualifierst::read(const typet &src)
 
   if(src.get_bool(ID_C_transparent_union))
     is_transparent_union=true;
+
+  if(src.get_bool(ID_C_noreturn))
+    is_noreturn=true;
 }
 
 /*******************************************************************\
@@ -131,6 +137,11 @@ void c_qualifierst::write(typet &dest) const
     dest.set(ID_C_transparent_union, true);
   else
     dest.remove(ID_C_transparent_union);
+
+  if(is_noreturn)
+    dest.set(ID_C_noreturn, true);
+  else
+    dest.remove(ID_C_noreturn);
 }
 
 /*******************************************************************\
@@ -153,6 +164,7 @@ void c_qualifierst::clear(typet &dest)
   dest.remove(ID_C_ptr32);
   dest.remove(ID_C_ptr64);
   dest.remove(ID_C_transparent_union);
+  dest.remove(ID_C_noreturn);
 }
 
 /*******************************************************************\

src/ansi-c/c_qualifiers.h

@@ -35,10 +35,11 @@ class c_qualifierst
     is_atomic=false;
     is_ptr32=is_ptr64=false;
     is_transparent_union=false;
+    is_noreturn=false;
   }
 
   // standard ones
-  bool is_constant, is_volatile, is_restricted, is_atomic;
+  bool is_constant, is_volatile, is_restricted, is_atomic, is_noreturn;
 
   // MS Visual Studio extension
   bool is_ptr32, is_ptr64;
@@ -61,7 +62,8 @@ class c_qualifierst
            (!is_restricted || q.is_restricted) &&
            (!is_atomic || q.is_atomic) &&
            (!is_ptr32 || q.is_ptr32) &&
-           (!is_ptr64 || q.is_ptr64);
+           (!is_ptr64 || q.is_ptr64) &&
+           (!is_noreturn || q.is_noreturn);
 
     // is_transparent_union isn't checked
   }
@@ -76,7 +78,8 @@ class c_qualifierst
            a.is_atomic==b.is_atomic &&
            a.is_ptr32==b.is_ptr32 &&
            a.is_ptr64==b.is_ptr64 &&
-           a.is_transparent_union==b.is_transparent_union;
+           a.is_transparent_union==b.is_transparent_union &&
+           a.is_noreturn==b.is_noreturn;
   }
 
   friend bool operator != (
@@ -96,13 +99,14 @@ class c_qualifierst
     is_ptr32|=b.is_ptr32;
     is_ptr64|=b.is_ptr64;
     is_transparent_union|=b.is_transparent_union;
+    is_noreturn|=b.is_noreturn;
     return *this;
   }
 
   friend unsigned count(const c_qualifierst &q)
   {
     return q.is_constant+q.is_volatile+q.is_restricted+q.is_atomic+
-           q.is_ptr32+q.is_ptr64;
+           q.is_ptr32+q.is_ptr64+q.is_noreturn;
   }
 };
 

src/ansi-c/parser.y

@@ -1518,6 +1518,8 @@ gcc_type_attribute:
         { $$=$1; set($$, ID_gcc_attribute_mode); stack($$).set(ID_size, stack($3).get(ID_identifier)); }
         | TOK_GCC_ATTRIBUTE_GNU_INLINE TOK_GCC_ATTRIBUTE_END
         { $$=$1; set($$, ID_static); } /* GCC extern inline - cleanup in ansi_c_declarationt::to_symbol */
+        | TOK_NORETURN
+        { $$=$1; set($$, ID_noreturn); }
         | gcc_attribute_specifier
         ;
 

src/ansi-c/type2name.cpp

@@ -124,6 +124,9 @@ static std::string type2name(
   if(type.get_bool(ID_C_transparent_union))
     result+='t';
 
+  if(type.get_bool(ID_C_noreturn))
+    result+='n';
+
   // this isn't really a qualifier, but the linker needs to
   // distinguish these - should likely be fixed in the linker instead
   if(!type.source_location().get_function().empty())

src/util/irep_ids.txt

@@ -393,7 +393,6 @@ C_qualifier #qualifier
 C_ptr32 #ptr32
 C_ptr64 #ptr64
 C_atomic #atomic
-C_noreturn #noreturn
 restrict
 byte_extract_big_endian
 byte_extract_little_endian
@@ -711,3 +710,5 @@ force
 release
 popcount
 function_type
+noreturn
+C_noreturn #noreturn