Merge pull request #62 from goblint/static_assert

Add support for `_Static_assert`

Author: michael-schwarz

src/frontc/cabs.ml

@@ -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

@@ -6394,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

@@ -169,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

@@ -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
@@ -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] }
@@ -1051,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] }

src/frontc/cprint.ml

@@ -899,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-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;
+}

test/testcil.pl

@@ -698,6 +698,7 @@ sub addToGroup {
 addTest("testrunc11/c11-extendedFloat");
 addTest("testrunc11/c11-noreturn");
 addTest("testrunc11/c11-atomic");
+addTest("testrunc11/c11-static-assert");
 addTest("testrunc11/gcc-c11-generic-1");
 # TODO: these messages are not even checked?
 addTestFail("testc11/gcc-c11-generic-2-1", "Multiple defaults in generic");