diff --git a/share/libc/assert.h b/share/libc/assert.h
index 0886eac92d58bb02635d595448dcc83ba4f914bb..4e7618753ef4fa94d167e7b9e6211a34a5530cbf 100644
--- a/share/libc/assert.h
+++ b/share/libc/assert.h
@@ -34,6 +34,9 @@ __BEGIN_DECLS
*/
extern void __FC_assert(int c, const char* file, int line, const char*expr);
+#define static_assert _Static_assert
+
+
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 5745e3cc4ab7dedb8ed30f51c166cdbf558ab511..b0b9065d0ad1d66ccb4cc844c21e4b44e901fdeb 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -161,6 +161,16 @@ let init_lexicon _ =
"_Noreturn is a C11 keyword, use -c11 option to enable it");
IDENT "_Noreturn"
end);
+ ("_Static_assert",
+ fun loc ->
+ if Kernel.C11.get () then STATIC_ASSERT loc
+ else begin
+ Kernel.(
+ warning
+ ~wkey:wkey_conditional_feature
+ "_Static_assert is a C11 keyword, use -c11 option to enable it");
+ IDENT "_Static_assert"
+ end);
("__attribute__", fun loc -> ATTRIBUTE loc);
("__attribute", fun loc -> ATTRIBUTE loc);
("__blockattribute__", fun _ -> BLOCKATTRIBUTE);
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 11d9ae4dbcd3c6a7af92e7f44b7412d1a2585836..a026e11a65e3b1ba88b714d5dcac47287063a257 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -368,7 +368,7 @@ let in_ghost_block ?(battrs=[]) l =
%token<Cabs.cabsloc> IF TRY EXCEPT FINALLY
%token ELSE
-%token<Cabs.cabsloc> ATTRIBUTE INLINE NORETURN ASM TYPEOF FUNCTION__ PRETTY_FUNCTION__
+%token<Cabs.cabsloc> ATTRIBUTE INLINE NORETURN STATIC_ASSERT ASM TYPEOF FUNCTION__ PRETTY_FUNCTION__
%token LABEL__
%token<Cabs.cabsloc> BUILTIN_VA_ARG
%token BLOCKATTRIBUTE
@@ -1080,6 +1080,14 @@ declaration: /* ISO 6.7.*/
{ doDeclaration (Some $1) ((snd $2)) (fst $2) $3 }
| SPEC decl_spec_list SEMICOLON
{ doDeclaration (Some $1) ((snd $2)) (fst $2) [] }
+| STATIC_ASSERT LPAREN expression RPAREN
+ {
+ STATIC_ASSERT ($3, "", $1)
+ }
+| STATIC_ASSERT LPAREN expression COMMA string_constant RPAREN
+ {
+ STATIC_ASSERT ($3, fst $5, $1)
+ }
;
init_declarator_list: /* ISO 6.7 */
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 75665dec0631f0844c434e7dacb8be41d85acee8..9ca6025872c6f0272e67affc9c0a6a730f306c33 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9192,6 +9192,56 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
| _ -> Kernel.fatal ~current:true "Too many attributes in pragma"
end
+ | Cabs.STATIC_ASSERT (e, s, loc) -> begin
+ let make_static_assert_vi_and_init ~global cond_exp =
+ (* pick a different name per call, to avoid typing issues;
+ the actual name is never used anyway *)
+ let vname, _ = newAlphaName false global "" "_Static_assert" in
+ let vi =
+ if global then
+ makeGlobalVar ~temp:false ~referenced:true vname intType
+ else
+ makeVarinfo ~source:false ~referenced:true false false vname intType
+ in
+ let attr name = Attr (name, []) in
+ vi.vattr <-
+ Cil.addAttributes [attr "FC_BUILTIN"; attr "_STATIC_ASSERT"] vi.vattr;
+ let exp =
+ (* create an arbitrary expression using a binary operator and
+ SizeOfStr for typing purposes only; the pretty-printer in
+ Cil_printer will desugar it as intended. *)
+ new_exp ~loc
+ (BinOp (PlusA, cond_exp, new_exp ~loc (SizeOfStr s), voidType))
+ in
+ vi, SingleInit exp
+ in
+ CurrentLoc.set (convLoc loc);
+ let (_, _, cond_exp, _) = doExp local_env CConst e ADrop in
+ begin
+ match Cil.constFoldToInt ~machdep:true cond_exp with
+ | Some i ->
+ if Integer.(equal i zero) then
+ Kernel.error ~current:true "static assertion failed%s%s@."
+ (if s <> "" then ": " else "") s
+ | None ->
+ Kernel.error ~current:true
+ "failed to evaluate constant expression in static assertion:@ \
+ @[%a@]"
+ Cprint.print_expression e
+ end;
+ if isglobal then begin
+ let vi, init = make_static_assert_vi_and_init true cond_exp in
+ cabsPushGlobal
+ (GVar (vi, { init = Some init}, loc));
+ empty
+ end
+ else
+ let vi, init = make_static_assert_vi_and_init false cond_exp in
+ let instr = mkStmtOneInstr (Local_init (vi, AssignInit init, loc)) in
+ !currentFunctionFDEC.slocals <- !currentFunctionFDEC.slocals @ [vi];
+ local_var_chunk (i2c (instr,[],[],[])) vi
+ end
+
| Cabs.FUNDEF (spec,((specs,(n,dt,a, _)) : Cabs.single_name),
(body : Cabs.block), loc1, loc2) when isglobal ->
begin
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index fbcdd4854b795ce496e5ba8bc6a0563d77bb1fa2..e337f84b87d1eadee03de099f4f2314347e842e0 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -182,6 +182,8 @@ and pp_def fmt = function
fprintf fmt "@[<hov 2>GLOBASM %s, loc(%a)@]" s pp_cabsloc loc
| PRAGMA (exp, loc) ->
fprintf fmt "@[<hov 2>PRAGMA exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
+ | STATIC_ASSERT (exp, s, loc) ->
+ fprintf fmt "@[<hov 2>STATIC_ASSERT exp(%a, %s, loc(%a))@]" pp_exp exp s pp_cabsloc loc
| LINKAGE (s, loc, defs) ->
fprintf fmt "@[<hov 2>LINKAGE %s, loc(%a), defs(" s pp_cabsloc loc;
List.iter (fun def -> fprintf fmt ",@ def(%a)" pp_def def) defs;
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 2afe7bfc31ffbf04f057b23e73ad4d9f9cccd5cd..efa88062efff9de170623a371a19c1e85f5f8884 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1043,6 +1043,16 @@ class cil_printer () = object (self)
instr_terminator
end
+ | Local_init(vi, AssignInit (SingleInit {
+ enode = BinOp (_, cond_exp, {enode = SizeOfStr s}, _)}), _) when
+ Cil.hasAttribute "_STATIC_ASSERT" vi.vattr ->
+ (* Hijack pretty-printer for a local _Static_assert *)
+ if s = "" then
+ fprintf fmt "@[<2>_Static_assert(%a)%s@]@\n"
+ self#exp cond_exp instr_terminator
+ else
+ fprintf fmt "@[<2>_Static_assert(%a, \"%s\")%s@]@\n"
+ self#exp cond_exp s instr_terminator
| Local_init(vi, AssignInit i, _) ->
Format.fprintf fmt "@[<2>%a =@ %a%s@]"
self#vdecl vi self#init i instr_terminator
@@ -1380,7 +1390,10 @@ class cil_printer () = object (self)
(* [JS 2012/12/07] could directly call self#attributesGen whenever we are
sure than it puts its printing material inside a box *)
fprintf fmt "@[%a@]" (self#attributesGen true) blk.battrs;
- let locals_decl = List.filter (fun v -> not v.vdefined) blk.blocals in
+ let visible_decl v =
+ not (v.vdefined || Cil.hasAttribute "_STATIC_ASSERT" v.vattr)
+ in
+ let locals_decl = List.filter (fun v -> visible_decl v) blk.blocals in
if locals_decl <> [] then
Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@;" ~suf:"@]@ "
self#vdecl_complete fmt locals_decl;
@@ -1778,6 +1791,20 @@ class cil_printer () = object (self)
fprintf fmt "%a %a;@\n"
self#pp_keyword (if comp.cstruct then "struct" else "union")
self#varname comp.cname
+ | GVar (vi, {init = Some (SingleInit {
+ enode = BinOp (_, cond_exp, { enode = SizeOfStr s }, _) })}, l)
+ when Cil.hasAttribute "_STATIC_ASSERT" vi.vattr ->
+ (* Hijack pretty-printer for a global _Static_assert *)
+ self#line_directive ~forcefile:true fmt l;
+ Format.fprintf fmt "@[<hov 2>";
+ if s = "" then
+ fprintf fmt "_Static_assert(%a)"
+ self#exp cond_exp
+ else
+ fprintf fmt "_Static_assert(%a, \"%s\")"
+ self#exp cond_exp s;
+ fprintf fmt ";";
+ fprintf fmt "@]@\n";
| GVar (vi, io, l) ->
self#line_directive ~forcefile:true fmt l;
Format.fprintf fmt "@[<hov 2>";
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 3633b1c43ff50c5db28a42b111ddadfcdb753917..af3a8d8bc22123af81f03646bfb1e09484738eba 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -624,6 +624,9 @@ and print_def fmt def =
| PRAGMA (a,_) ->
fprintf fmt "@[#pragma %a@]@\n" print_expression a
+ | STATIC_ASSERT (e, s, _) ->
+ fprintf fmt "@[_Static_assert (%a, %s)@]@\n" print_expression e s
+
| LINKAGE (n, _, dl) ->
fprintf fmt "@[<2>extern@ %s@ {%a@;}@]" n (pp_list print_def) dl
diff --git a/src/kernel_services/parsetree/cabs.mli b/src/kernel_services/parsetree/cabs.mli
index 9294f5b774a046acd314a3f31fe882fd28e07fb2..bed5b26fa88f783bee4086049161e886a340f62f 100644
--- a/src/kernel_services/parsetree/cabs.mli
+++ b/src/kernel_services/parsetree/cabs.mli
@@ -169,6 +169,7 @@ and definition =
| ONLYTYPEDEF of specifier * cabsloc
| GLOBASM of string * cabsloc
| PRAGMA of expression * cabsloc
+ | STATIC_ASSERT of expression * string * cabsloc
| LINKAGE of string * cabsloc * definition list (* extern "C" { ... } *)
| GLOBANNOT of Logic_ptree.decl list
(** Logical declaration (axiom, logic, etc.)*)
diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml
index 6ceeedb4f04e8a71592880ba5ac3cd10a2f01561..14b0e66acbc617f9be372a6d9cc3eeef6287c106 100644
--- a/src/kernel_services/parsetree/cabshelper.ml
+++ b/src/kernel_services/parsetree/cabshelper.ml
@@ -156,6 +156,7 @@ let get_definitionloc (d : definition) : cabsloc =
| ONLYTYPEDEF(_, l) -> l
| GLOBASM(_, l) -> l
| PRAGMA(_, l) -> l
+ | STATIC_ASSERT (_, _, l) -> l
| LINKAGE (_, l, _) -> l
| GLOBANNOT({Logic_ptree.decl_loc = l }::_) -> l
| GLOBANNOT [] -> assert false
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index 1783feb0a22c113b7f41dc73a786a520562b507c..626bd95333d302625f998deb0655dc1cd604f3e9 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -257,6 +257,9 @@ and childrenDefinition vis d =
| PRAGMA (e, l) ->
let e' = visitCabsExpression vis e in
if e' != e then PRAGMA (e', l) else d
+ | STATIC_ASSERT (e, s, l) ->
+ let e' = visitCabsExpression vis e in
+ if e' != e then STATIC_ASSERT (e', s, l) else d
| LINKAGE (n, l, dl) ->
let dl' = mapNoCopyList (visitCabsDefinition vis) dl in
if dl' != dl then LINKAGE (n, l, dl') else d
diff --git a/src/plugins/metrics/metrics_cabs.ml b/src/plugins/metrics/metrics_cabs.ml
index 5f7929d605735f42fd156d47c60b687ab3f8e295..315698ea973cbc168f0fd59e634f9b33257602a9 100644
--- a/src/plugins/metrics/metrics_cabs.ml
+++ b/src/plugins/metrics/metrics_cabs.ml
@@ -114,6 +114,7 @@ class metricsCabsVisitor = object(self)
| ONLYTYPEDEF _
| GLOBASM _
| PRAGMA _
+ | STATIC_ASSERT _
| LINKAGE _
| CUSTOM _
| GLOBANNOT _ -> Cil.DoChildren;
diff --git a/tests/syntax/oracle/static_assert.0.res.oracle b/tests/syntax/oracle/static_assert.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0a7afa853d393a80053219c13c434eb461c32f4c
--- /dev/null
+++ b/tests/syntax/oracle/static_assert.0.res.oracle
@@ -0,0 +1,21 @@
+[kernel] Parsing tests/syntax/static_assert.c (with preprocessing)
+/* Generated by Frama-C */
+#include "assert.h"
+_Static_assert(1, "string");
+_Static_assert(2);
+int main(void)
+{
+ int __retres;
+ _Static_assert(sizeof(int) > sizeof(char), "int must be greater than char");
+
+ int ret = 42;
+ _Static_assert(3);
+
+ __retres = ret;
+ goto return_label;
+ _Static_assert(4, "after return");
+
+ return_label: return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/static_assert.1.res.oracle b/tests/syntax/oracle/static_assert.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ccc5ea39b44fd70bb24ca71d78f991b6d0c654c1
--- /dev/null
+++ b/tests/syntax/oracle/static_assert.1.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing tests/syntax/static_assert.c (with preprocessing)
+[kernel] tests/syntax/static_assert.c:12: User Error:
+ static assertion failed: fail
+[kernel] tests/syntax/static_assert.c:22: User Error:
+ failed to evaluate constant expression in static assertion:
+ a == 42
+[kernel] tests/syntax/static_assert.c:35: User Error: static assertion failed
+[kernel] User Error: stopping on file "tests/syntax/static_assert.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/static_assert.c b/tests/syntax/static_assert.c
new file mode 100644
index 0000000000000000000000000000000000000000..5d856c29e48456c03c34ee6c0aa796978997100f
--- /dev/null
+++ b/tests/syntax/static_assert.c
@@ -0,0 +1,36 @@
+/* run.config
+ STDOPT: #"-c11"
+ EXIT: 1
+ STDOPT: #"-c11 -cpp-extra-args=-DFAIL"
+*/
+
+_Static_assert(1, "string");
+
+#include <assert.h>
+
+#ifdef FAIL
+static_assert(0, "fail");
+#endif
+
+_Static_assert(2); // without message string
+
+int main() {
+ static_assert(sizeof(int) > sizeof(char), "int must be greater than char");
+
+#ifdef FAIL
+ int a = 42;
+ static_assert(a == 42, "non-static condition");
+#endif
+
+ int ret = 42;
+
+ static_assert(3); // between statements
+
+ return ret;
+
+ _Static_assert(4, "after return");
+}
+
+#ifdef FAIL
+static_assert(0); // fail without message string
+#endif