Merge branch 'extended_float_types' into develop

Author: michael-schwarz

src/cil.ml

@@ -4278,7 +4278,8 @@ class defaultCilPrinterClass : cilPrinter = object (self)
   method pAttr (Attr(an, args): attribute) : doc * bool =
     (* Recognize and take care of some known cases *)
     match an, args with
-      "const", [] -> nil, false (* don't print const directly, because of split local declarations *)
+      "atomic", [] -> text "_Atomic", false
+    | "const", [] -> nil, false (* don't print const directly, because of split local declarations *)
     | "pconst", [] -> text "const", false (* pconst means print const *)
           (* Put the aconst inside the attribute list *)
     | "complex", [] when !c99Mode -> text "_Complex", false

src/frontc/cabs.ml

@@ -96,7 +96,7 @@ and funspec =
     INLINE | VIRTUAL | EXPLICIT
 
 and cvspec =
-    CV_CONST | CV_VOLATILE | CV_RESTRICT | CV_COMPLEX
+    CV_CONST | CV_VOLATILE | CV_RESTRICT | CV_COMPLEX | CV_ATOMIC
 
 (* Type specifier elements. These appear at the start of a declaration *)
 (* Everywhere they appear in this file, they appear as a 'spec_elem list', *)
@@ -185,6 +185,7 @@ and definition =
  | TRANSFORMER of definition * definition list * cabsloc
  (* expression transformer: source and destination *)
  | EXPRTRANSFORMER of expression * expression * cabsloc
+ | STATIC_ASSERT of expression * string * cabsloc
 
 
 (* the string is a file name, and then the list of toplevel forms *)

src/frontc/cabs2cil.ml

@@ -2704,6 +2704,7 @@ and convertCVtoAttr (src: A.cvspec list) : A.attribute list =
   | CV_VOLATILE :: tl -> ("volatile",[]) :: (convertCVtoAttr tl)
   | CV_RESTRICT :: tl -> ("restrict",[]) :: (convertCVtoAttr tl)
   | CV_COMPLEX  :: tl -> ("complex",[]) ::  (convertCVtoAttr tl)
+  | CV_ATOMIC   :: tl -> ("atomic",[]) ::  (convertCVtoAttr tl)
 
 
 and makeVarInfoCabs
@@ -6393,7 +6394,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function
             E.s (bug "doDecl returns non-empty statement for global"))
         dl;
       empty
-
+  | STATIC_ASSERT _ -> empty
   | _ -> E.s (error "unexpected form of declaration")
 
 and doTypedef ((specs, nl): A.name_group) =

src/frontc/cabshelper.ml

@@ -6,7 +6,7 @@ let getident () =
     nextident := !nextident + 1;
     !nextident
 
-let currentLoc () = 
+let currentLoc () =
   let l, f, c, lc = Errormsg.getPosition () in
   { lineno   = l;
     filename = f;
@@ -17,8 +17,8 @@ let currentLoc () =
     endByteno = -1;
     endColumnno = -1;}
 
-let cabslu = {lineno = -10; 
-	      filename = "cabs loc unknown"; 
+let cabslu = {lineno = -10;
+	      filename = "cabs loc unknown";
 	      byteno = -10; columnno = -10;
               ident = 0;
               endLineno = -10; endByteno = -10; endColumnno = -10;}
@@ -27,9 +27,9 @@ let string_of_loc l =
   Printf.sprintf "%s:%d:%d-%d:%d" l.filename l.lineno l.columnno l.endLineno l.endColumnno
 
 let joinLoc l1 l2 = match l1, l2 with
-  | l1, l2 when l1.filename = l2.filename && l1.endByteno < 0 && l2.endByteno < 0 && l1.byteno <= l2.byteno -> 
+  | l1, l2 when l1.filename = l2.filename && l1.endByteno < 0 && l2.endByteno < 0 && l1.byteno <= l2.byteno ->
     {l1 with endLineno = l2.lineno; endByteno = l2.byteno; endColumnno = l2.columnno}
-  | l1, l2 when l1.filename = l2.filename && l1.endByteno = l2.endByteno && l1.byteno = l2.byteno -> 
+  | l1, l2 when l1.filename = l2.filename && l1.endByteno = l2.endByteno && l1.byteno = l2.byteno ->
     l1 (* alias fundefs *)
   | _, _ ->
     (* some code generators leave start and end into different files: https://github.com/goblint/cil/issues/54 *)
@@ -76,6 +76,7 @@ let get_definitionloc (d : definition) : cabsloc =
   | TRANSFORMER(_, _, l) -> l
   | EXPRTRANSFORMER(_, _, l) -> l
   | LINKAGE (_, l, _) -> l
+  | STATIC_ASSERT (_,_,l) -> l
 
 let get_statementloc (s : statement) : cabsloc =
 begin
@@ -103,23 +104,23 @@ begin
 end
 
 
-let explodeStringToInts (s: string) : int64 list =  
-  let rec allChars i acc = 
+let explodeStringToInts (s: string) : int64 list =
+  let rec allChars i acc =
     if i < 0 then acc
     else allChars (i - 1) (Int64.of_int (Char.code (String.get s i)) :: acc)
   in
   allChars (-1 + String.length s) []
 
 let valueOfDigit chr =
-  let int_value = 
+  let int_value =
     match chr with
       '0'..'9' -> (Char.code chr) - (Char.code '0')
     | 'a'..'z' -> (Char.code chr) - (Char.code 'a') + 10
     | 'A'..'Z' -> (Char.code chr) - (Char.code 'A') + 10
     | _ -> Errormsg.s (Errormsg.bug "not a digit") in
   Int64.of_int int_value
-  
-    
+
+
 open Pretty
-let d_cabsloc () cl = 
+let d_cabsloc () cl =
   text cl.filename ++ text ":" ++ num cl.lineno

src/frontc/cabsvisit.ml

@@ -325,7 +325,8 @@ and childrenDefinition vis d =
   | LINKAGE (n, l, dl) ->
       let dl' = mapNoCopyList (visitCabsDefinition vis) dl in
       if dl' != dl then LINKAGE (n, l, dl') else d
-
+  
+  | STATIC_ASSERT _ -> d
   | TRANSFORMER _ -> d
   | EXPRTRANSFORMER _ -> d
 

src/frontc/clexer.mll

@@ -119,6 +119,7 @@ let init_lexicon _ =
       ("const", fun loc -> CONST loc);
       ("__const", fun loc -> CONST loc);
       ("__const__", fun loc -> CONST loc);
+      ("_Atomic", fun loc -> ATOMIC loc);
       ("_Complex", fun loc -> COMPLEX loc);
       ("__complex__", fun loc -> COMPLEX loc);
       ("static", fun loc -> STATIC loc);
@@ -168,6 +169,7 @@ let init_lexicon _ =
       ("__inline", fun loc -> INLINE loc);
       ("_inline", fun loc -> IDENT ("_inline", loc));
       ("_Noreturn", fun loc -> NORETURN loc);
+      ("_Static_assert", fun loc -> STATIC_ASSERT loc);
       ("__attribute__", fun loc -> ATTRIBUTE loc);
       ("__attribute", fun loc -> ATTRIBUTE loc);
 (*

src/frontc/cparser.mly

@@ -257,7 +257,7 @@ let transformOffsetOf (speclist, dtype) member =
 %token<Cabs.cabsloc> GENERIC NORETURN /* C11 */
 %token<Cabs.cabsloc> ENUM STRUCT TYPEDEF UNION
 %token<Cabs.cabsloc> SIGNED UNSIGNED LONG SHORT
-%token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
+%token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST ATOMIC RESTRICT AUTO REGISTER
 %token<Cabs.cabsloc> THREAD
 
 %token<Cabs.cabsloc> SIZEOF ALIGNOF
@@ -290,7 +290,7 @@ let transformOffsetOf (speclist, dtype) member =
 %token<Cabs.cabsloc> IF
 %token ELSE
 
-%token<Cabs.cabsloc> ATTRIBUTE INLINE ASM TYPEOF REAL IMAG FUNCTION__ PRETTY_FUNCTION__ CLASSIFYTYPE
+%token<Cabs.cabsloc> ATTRIBUTE INLINE STATIC_ASSERT ASM TYPEOF REAL IMAG FUNCTION__ PRETTY_FUNCTION__ CLASSIFYTYPE
 %token LABEL__
 %token<Cabs.cabsloc> BUILTIN_VA_ARG ATTRIBUTE_USED
 %token BUILTIN_VA_LIST
@@ -323,7 +323,7 @@ let transformOffsetOf (speclist, dtype) member =
 %left	INF SUP INF_EQ SUP_EQ
 %left	INF_INF SUP_SUP
 %left	PLUS MINUS
-%left	STAR SLASH PERCENT CONST RESTRICT VOLATILE COMPLEX
+%left	STAR SLASH PERCENT CONST RESTRICT ATOMIC VOLATILE COMPLEX
 %right	EXCLAM TILDE PLUS_PLUS MINUS_MINUS CAST RPAREN ADDROF SIZEOF ALIGNOF IMAG REAL CLASSIFYTYPE
 %left 	LBRACKET
 %left	DOT ARROW LPAREN LBRACE
@@ -930,6 +930,21 @@ declaration:                                /* ISO 6.7.*/
                                        { doDeclaration (joinLoc (snd $1) $3) (fst $1) $2 }
 |   decl_spec_list SEMICOLON
                                        { doDeclaration (joinLoc (snd $1) $2) (fst $1) [] }
+|   static_assert_declaration          { let (e, m, loc) = $1 in STATIC_ASSERT (e, m, loc) }
+;
+
+static_assert_declaration:
+
+|   STATIC_ASSERT LPAREN expression RPAREN /* C23 */
+      {
+        (fst $3, "", $1)
+      }
+|   STATIC_ASSERT LPAREN expression COMMA string_constant RPAREN
+      {
+        (fst $3, fst $5, $1)
+      }
+;
+
 ;
 init_declarator_list:                       /* ISO 6.7 */
     init_declarator                              { [$1] }
@@ -951,9 +966,11 @@ decl_spec_list:                         /* ISO 6.7 */
 |   REGISTER decl_spec_list_opt         { SpecStorage REGISTER :: $2, $1}
                                         /* ISO 6.7.2 */
 |   type_spec decl_spec_list_opt_no_named { SpecType (fst $1) :: $2, snd $1 }
+|   ATOMIC LPAREN decl_spec_list RPAREN decl_spec_list_opt_no_named { (fst $3) @ SpecCV(CV_ATOMIC) :: $5, $1 }
                                         /* ISO 6.7.4 */
 |   INLINE decl_spec_list_opt           { SpecInline :: $2, $1 }
 |   NORETURN decl_spec_list_opt         { SpecNoreturn  :: $2, $1 }
+
 |   cvspec decl_spec_list_opt           { (fst $1) :: $2, snd $1 }
 |   attribute_nocv decl_spec_list_opt   { SpecAttr (fst $1) :: $2, snd $1 }
 /* specifier pattern variable (must be last in spec list) */
@@ -1049,6 +1066,15 @@ struct_decl_list: /* (* ISO 6.7.2. Except that we allow empty structs. We
 
 |  error                          SEMICOLON struct_decl_list
                                           { $3 }
+/*(* C11 allows static_assert-declaration *)*/
+|  static_assert_declaration             {
+       []
+   }
+
+|  static_assert_declaration      SEMICOLON struct_decl_list  {
+       $3
+   }
+
 ;
 field_decl_list: /* (* ISO 6.7.2 *) */
     field_decl                           { [$1] }
@@ -1294,6 +1320,7 @@ cvspec:
 |   VOLATILE                            { SpecCV(CV_VOLATILE), $1 }
 |   RESTRICT                            { SpecCV(CV_RESTRICT), $1 }
 |   COMPLEX                             { SpecCV(CV_COMPLEX), $1 }
+|   ATOMIC                              { SpecCV(CV_ATOMIC), $1 }
 ;
 
 /*** GCC attributes ***/

src/frontc/cprint.ml

@@ -148,7 +148,9 @@ let rec print_specifiers (specs: spec_elem list) =
         | CV_CONST -> "const"
         | CV_VOLATILE -> "volatile"
         | CV_RESTRICT -> "restrict"
-        | CV_COMPLEX -> "complex")
+        | CV_COMPLEX -> "complex"
+        | CV_ATOMIC -> "_Atomic"
+        )
     | SpecAttr al -> print_attribute al; space ()
     | SpecType bt -> print_type_spec bt
     | SpecPattern name -> printl ["@specifier";"(";name;")"]
@@ -897,6 +899,13 @@ and print_def def =
       print " }";
       force_new_line()
 
+  | STATIC_ASSERT(e,str,loc) ->
+      setLoc(loc);
+      print "_Static_assert(";
+      print_expression e;
+      print ",";
+      print_string str;
+      print ");";
 
 (* sm: print a comment if the printComments flag is set *)
 and comprint (str : string) : unit =

test/small1/c11-atomic.c

@@ -0,0 +1,14 @@
+#include "testharness.h"
+#include <stdnoreturn.h>
+
+_Atomic const int * p1;  // p is a pointer to an atomic const int
+const _Atomic(int) * p3; // same
+_Atomic(int) const * p3;
+// _Atomic(int*) const  p4; // unsupported as of now
+
+typedef _Atomic _Bool atomic_bool;
+
+
+int main() {
+    SUCCESS;
+}

test/small1/c11-static-assert.c

@@ -0,0 +1,10 @@
+#include "testharness.h"
+#include <stdnoreturn.h>
+
+_Static_assert (2  <= 18, "blubb");
+
+
+int main() {
+    _Static_assert (2  <= 18, "blubb");
+    SUCCESS;
+}