From a8307d7bf2316a641c60e08f129218c15414f852 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Jan 2026 10:08:20 +0200 Subject: [PATCH 1/7] Add tests for _Static_assert failures --- test/small1/c11-static-assert-fail1.c | 7 +++++++ test/small1/c11-static-assert-fail2.c | 6 ++++++ test/testcil.pl | 2 ++ 3 files changed, 15 insertions(+) create mode 100644 test/small1/c11-static-assert-fail1.c create mode 100644 test/small1/c11-static-assert-fail2.c diff --git a/test/small1/c11-static-assert-fail1.c b/test/small1/c11-static-assert-fail1.c new file mode 100644 index 000000000..494945216 --- /dev/null +++ b/test/small1/c11-static-assert-fail1.c @@ -0,0 +1,7 @@ +#include "testharness.h" + +_Static_assert (2 > 18, "blubb"); + +int main() { + SUCCESS; +} diff --git a/test/small1/c11-static-assert-fail2.c b/test/small1/c11-static-assert-fail2.c new file mode 100644 index 000000000..6e7b61bf0 --- /dev/null +++ b/test/small1/c11-static-assert-fail2.c @@ -0,0 +1,6 @@ +#include "testharness.h" + +int main() { + _Static_assert (2 > 18, "blubb"); + SUCCESS; +} diff --git a/test/testcil.pl b/test/testcil.pl index ec7259669..46e104e77 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -738,6 +738,8 @@ sub addToGroup { addTest("testrunc11/c11-atomic"); addTest("testrunc11/c11-atomic-store"); addTest("testrunc11/c11-static-assert"); +addTestFail("testrunc11/c11-static-assert-fail1", "Global _Static_assert fails"); +addTestFail("testrunc11/c11-static-assert-fail2", "Local _Static_assert fails"); addTest("testrunc11/c11-align-of"); addTest("testrunc11/gcc-c11-generic-1"); # TODO: these messages are not even checked? From 54f841a65cee8a99992560588180846bed632eb5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Jan 2026 10:16:01 +0200 Subject: [PATCH 2/7] Add tests for _Static_assert without message --- test/small1/c11-static-assert.c | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/test/small1/c11-static-assert.c b/test/small1/c11-static-assert.c index a097a8d01..8eb716e99 100644 --- a/test/small1/c11-static-assert.c +++ b/test/small1/c11-static-assert.c @@ -1,10 +1,11 @@ #include "testharness.h" #include -_Static_assert (2 <= 18, "blubb"); - +_Static_assert (2 <= 18); +_Static_assert (2 <= 18, "blubb"); int main() { - _Static_assert (2 <= 18, "blubb"); + _Static_assert (2 <= 18); + _Static_assert (2 <= 18, "blubb"); SUCCESS; } From 2ca00c2a55dcaf834aa3012e2e3282873f57810b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Jan 2026 10:20:02 +0200 Subject: [PATCH 3/7] Add tests for _Static_assert in struct --- test/small1/c11-static-assert-fail3.c | 10 ++++++++++ test/small1/c11-static-assert.c | 6 ++++++ test/testcil.pl | 1 + 3 files changed, 17 insertions(+) create mode 100644 test/small1/c11-static-assert-fail3.c diff --git a/test/small1/c11-static-assert-fail3.c b/test/small1/c11-static-assert-fail3.c new file mode 100644 index 000000000..70a68b722 --- /dev/null +++ b/test/small1/c11-static-assert-fail3.c @@ -0,0 +1,10 @@ +#include "testharness.h" + +struct S { + int x; + _Static_assert (2 > 18, "blubb"); +}; + +int main() { + SUCCESS; +} diff --git a/test/small1/c11-static-assert.c b/test/small1/c11-static-assert.c index 8eb716e99..8c098d7c9 100644 --- a/test/small1/c11-static-assert.c +++ b/test/small1/c11-static-assert.c @@ -4,6 +4,12 @@ _Static_assert (2 <= 18); _Static_assert (2 <= 18, "blubb"); +struct S { + int x; + _Static_assert (2 <= 18); + _Static_assert (2 <= 18, "blubb"); +}; + int main() { _Static_assert (2 <= 18); _Static_assert (2 <= 18, "blubb"); diff --git a/test/testcil.pl b/test/testcil.pl index 46e104e77..deb528983 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -740,6 +740,7 @@ sub addToGroup { addTest("testrunc11/c11-static-assert"); addTestFail("testrunc11/c11-static-assert-fail1", "Global _Static_assert fails"); addTestFail("testrunc11/c11-static-assert-fail2", "Local _Static_assert fails"); +addTestFail("testrunc11/c11-static-assert-fail3", "Struct _Static_assert fails"); addTest("testrunc11/c11-align-of"); addTest("testrunc11/gcc-c11-generic-1"); # TODO: these messages are not even checked? From e7c3c26e43ba278e6da16b2218fb94d641c29d88 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Jan 2026 10:24:26 +0200 Subject: [PATCH 4/7] Make _Static_assert string optional in Cabs --- src/frontc/cabs.ml | 2 +- src/frontc/cparser.mly | 4 ++-- src/frontc/cprint.ml | 8 ++++++-- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index 45491dc1a..fd46bfc5c 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -187,7 +187,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 + | STATIC_ASSERT of expression * string option * cabsloc (* the string is a file name, and then the list of toplevel forms *) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 112f423e1..ebd3ab528 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1005,11 +1005,11 @@ static_assert_declaration: | STATIC_ASSERT LPAREN expression RPAREN /* C23 */ { - (fst $3, "", $1) + (fst $3, None, $1) } | STATIC_ASSERT LPAREN expression COMMA const_raw_string RPAREN { - (fst $3, fst $5, $1) + (fst $3, Some (fst $5), $1) } ; diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 31a2257e2..919dc7e75 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -909,8 +909,12 @@ and print_def def = setLoc(loc); print "_Static_assert("; print_expression e; - print ","; - print_string str; + begin match str with + | Some str -> + print ","; + print_string str; + | None -> () + end; print ");"; (* sm: print a comment if the printComments flag is set *) From 28b60d4f653b33e5b558cf9908c845e222fc02e0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Jan 2026 10:38:56 +0200 Subject: [PATCH 5/7] Check _Static_assert (closes #65) --- src/frontc/cabs2cil.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index fd6e239ce..6cb1f7bdc 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6615,7 +6615,19 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function E.s (bug "doDecl returns non-empty statement for global")) dl; empty - | STATIC_ASSERT _ -> empty + | STATIC_ASSERT (e, str, loc) -> + if isglobal || isstmt then + currentLoc := convLoc loc; + currentExpLoc := convLoc loc; + let d_message () = function + | None -> nil + | Some str -> dprintf ": %s" str + in + begin match isIntegerConstant e with + | Some 0 -> E.s (error "Static assert failed at %a%a" d_loc !currentLoc d_message str) + | Some _ -> empty + | None -> E.s (error "Static assert with a non-constant at %a%a" d_loc !currentLoc d_message str) + end | _ -> E.s (error "unexpected form of declaration") and doTypedef ((specs, nl): A.name_group) = From 32e7c437f06ab06c267805c2ba352101ab8f87ca Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Jan 2026 10:40:07 +0200 Subject: [PATCH 6/7] Implement _Static_assert in Cabsvisit --- src/frontc/cabsvisit.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index 444392e58..46319b059 100644 --- a/src/frontc/cabsvisit.ml +++ b/src/frontc/cabsvisit.ml @@ -321,7 +321,9 @@ and childrenDefinition vis d = let dl' = mapNoCopyList (visitCabsDefinition vis) dl in if dl' != dl then LINKAGE (n, l, dl') else d - | STATIC_ASSERT _ -> d + | STATIC_ASSERT (e, str, l) -> + let e' = visitCabsExpression vis e in + if e' != e then STATIC_ASSERT (e', str, l) else d | TRANSFORMER _ -> d | EXPRTRANSFORMER _ -> d From 52ba8d00c6369fc119c8ba5f9c3303d0897f1b89 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Jan 2026 11:09:30 +0200 Subject: [PATCH 7/7] Check _Static_assert in struct (closes #65) --- src/frontc/cabs.ml | 8 ++++++-- src/frontc/cabs2cil.ml | 19 +++++++++++++++++++ src/frontc/cabsvisit.ml | 13 +++++++++++-- src/frontc/cparser.mly | 12 +++++++----- src/frontc/cprint.ml | 16 ++++++++++++++-- src/frontc/patch.ml | 11 ++++++++--- 6 files changed, 65 insertions(+), 14 deletions(-) diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index fd46bfc5c..558503244 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -83,8 +83,8 @@ type typeSpecifier = (* Merge all specifiers into one type *) a forward declaration or simple reference to the type); they also have a list of __attribute__s that appeared between the keyword and the type name (definitions only) *) - | Tstruct of string * field_group list option * attribute list - | Tunion of string * field_group list option * attribute list + | Tstruct of string * struct_decl list option * attribute list + | Tunion of string * struct_decl list option * attribute list | Tenum of string * enum_item list option * attribute list | TtypeofE of expression (* GCC __typeof__ *) | TtypeofT of specifier * decl_type (* GCC __typeof__ *) @@ -150,6 +150,10 @@ and name_group = specifier * name list (* The optional expression is the bitfield *) and field_group = specifier * (name * expression option) list +and struct_decl = + | FIELD_GROUP of field_group + | FIELD_STATIC_ASSERT of expression * string option * cabsloc + (* like name_group, except the declared variables are allowed to have initializers *) (* e.g.: int x=1, y=2; *) and init_name_group = specifier * init_name list diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 6cb1f7bdc..a8132b106 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -2667,6 +2667,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of if n = "" then E.s (error "Missing struct tag on incomplete struct"); findCompType "struct" n [] | [A.Tstruct (n, Some nglist, extraAttrs)] -> (* A definition of a struct *) + let nglist = doStructDecls nglist in let (specs, names) = List.split nglist in let n' = if n <> "" then n else anonStructName "struct" suggestedAnonName specs in @@ -2678,6 +2679,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of if n = "" then E.s (error "Missing union tag on incomplete union"); findCompType "union" n [] | [A.Tunion (n, Some nglist, extraAttrs)] -> (* A definition of a union *) + let nglist = doStructDecls nglist in let (specs, names) = List.split nglist in let n' = if n <> "" then n else anonStructName "union" suggestedAnonName specs in @@ -2827,6 +2829,23 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of in bt,!storage,!isinline,List.rev (!attrs @ (convertCVtoAttr !cvattrs)) + +and doStructDecls (struct_decls: struct_decl list): field_group list = + List.filter_map (function + | FIELD_GROUP fg -> Some fg + | FIELD_STATIC_ASSERT (e, str, loc) -> + let loc = convLoc loc in + let d_message () = function + | None -> nil + | Some str -> dprintf ": %s" str + in + begin match isIntegerConstant e with + | Some 0 -> E.s (error "Static assert failed at %a%a" d_loc loc d_message str) + | Some _ -> None + | None -> E.s (error "Static assert with a non-constant at %a%a" d_loc loc d_message str) + end + ) struct_decls + (* given some cv attributes, convert them into named attributes for uniform processing *) and convertCVtoAttr (src: A.cvspec list) : A.attribute list = diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index 46319b059..848aaefc4 100644 --- a/src/frontc/cabsvisit.ml +++ b/src/frontc/cabsvisit.ml @@ -189,13 +189,22 @@ and childrenTypeSpecifier vis ts = let nel' = mapNoCopy doOneField nel in if s' != s || nel' != nel then (s', nel') else input in + let childrenStructDecl input = + match input with + | FIELD_GROUP fg -> + let fg' = childrenFieldGroup fg in + if fg' != fg then FIELD_GROUP fg' else input + | FIELD_STATIC_ASSERT (e, str, l) -> + let e' = visitCabsExpression vis e in + if e' != e then FIELD_STATIC_ASSERT (e', str, l) else input + in match ts with Tstruct (n, Some fg, extraAttrs) -> (*(trace "sm" (dprintf "visiting struct %s\n" n));*) - let fg' = mapNoCopy childrenFieldGroup fg in + let fg' = mapNoCopy childrenStructDecl fg in if fg' != fg then Tstruct( n, Some fg', extraAttrs) else ts | Tunion (n, Some fg, extraAttrs) -> - let fg' = mapNoCopy childrenFieldGroup fg in + let fg' = mapNoCopy childrenStructDecl fg in if fg' != fg then Tunion( n, Some fg', extraAttrs) else ts | Tenum (n, Some ei, extraAttrs) -> let doOneEnumItem ((s, attrs, e, loc) as ei) = diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index ebd3ab528..aa6a01c86 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -370,7 +370,7 @@ let transformOffsetOf (speclist, dtype) member = %type decl_spec_list %type type_spec -%type struct_decl_list +%type struct_decl_list %type old_proto_decl @@ -1148,13 +1148,13 @@ struct_decl_list: /* (* ISO 6.7.2. Except that we allow empty structs. We */ /* empty */ { [] } | decl_spec_list SEMICOLON struct_decl_list - { (fst $1, + { FIELD_GROUP (fst $1, [(missingFieldDecl, None)]) :: $3 } /*(* GCC allows extra semicolons *)*/ | SEMICOLON struct_decl_list { $2 } | decl_spec_list field_decl_list SEMICOLON struct_decl_list - { (fst $1, $2) + { FIELD_GROUP (fst $1, $2) :: $4 } /*(* MSVC allows pragmas in strange places *)*/ | pragma struct_decl_list { $2 } @@ -1163,11 +1163,13 @@ struct_decl_list: /* (* ISO 6.7.2. Except that we allow empty structs. We { $3 } /*(* C11 allows static_assert-declaration *)*/ | static_assert_declaration { - [] + let (e, m, loc) = $1 in + [FIELD_STATIC_ASSERT (e, m, loc)] } | static_assert_declaration SEMICOLON struct_decl_list { - $3 + let (e, m, loc) = $1 in + FIELD_STATIC_ASSERT (e, m, loc) :: $3 } ; diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 919dc7e75..caaa42d57 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -244,13 +244,25 @@ and print_decl (n: string) = function comprint ")" -and print_fields (flds : field_group list) = +and print_fields (flds : struct_decl list) = if flds = [] then print " { } " else begin print " {"; indent (); List.iter - (fun fld -> print_field_group fld; print ";"; new_line ()) + (function + | FIELD_GROUP fld -> print_field_group fld; print ";"; new_line () + | FIELD_STATIC_ASSERT (e, str, loc) -> + print "_Static_assert("; + print_expression e; + begin match str with + | Some str -> + print ","; + print_string str; + | None -> () + end; + print ");"; + ) flds; unindent (); print "} " diff --git a/src/frontc/patch.ml b/src/frontc/patch.ml index 88839f571..10f6f361f 100644 --- a/src/frontc/patch.ml +++ b/src/frontc/patch.ml @@ -558,12 +558,17 @@ begin ) end -and unifyField (pat : field_group) (tgt : field_group) : binding list = +and unifyField (pat : struct_decl) (tgt : struct_decl) : binding list = begin - match pat,tgt with (spec1, list1), (spec2, list2) -> ( + match pat, tgt with + | FIELD_GROUP (spec1, list1), FIELD_GROUP (spec2, list2) -> (unifySpecifiers spec1 spec2) @ (unifyList list1 list2 unifyNameExprOpt) - ) + | FIELD_STATIC_ASSERT (exp1, str1, l1), FIELD_STATIC_ASSERT (exp2, str2, l2) -> + (unifyExpr exp1 exp2) + | _, _ -> + if verbose then (trace "patchDebug" (dprintf "mismatching struct_decl-s\n")); + raise NoMatch end and unifyNameExprOpt (pat : name * expression option)