From 2f4b4fabbc7b030bcc9e238e1d54f046973d115c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 16 Dec 2021 13:55:09 +0100 Subject: [PATCH 1/3] Support for C11 _Noreturn Co-authored-by: Baris Coslu --- src/frontc/cabs.ml | 1 + src/frontc/cabs2cil.ml | 1 + src/frontc/cabsvisit.ml | 2 +- src/frontc/clexer.mll | 1 + src/frontc/cparser.mly | 5 +++-- src/frontc/cprint.ml | 5 +++-- test/small1/c11-noreturn.c | 24 ++++++++++++++++++++++++ test/small1/gcc-c11-generic-1.c | 7 +++---- test/testcil.pl | 1 + 9 files changed, 38 insertions(+), 9 deletions(-) create mode 100644 test/small1/c11-noreturn.c diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index 0f0409541..b073dd1e3 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -105,6 +105,7 @@ and spec_elem = | SpecAttr of attribute (* __attribute__ *) | SpecStorage of storage | SpecInline + | SpecNoreturn | SpecType of typeSpecifier | SpecPattern of string (* specifier pattern variable *) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 7ce6ad170..015c74d45 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -2333,6 +2333,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of match se with A.SpecTypedef -> acc | A.SpecInline -> isinline := true; acc + | A.SpecNoreturn -> attrs := ("noreturn", []) :: !attrs; acc | A.SpecStorage st -> if !storage <> NoStorage then E.s (error "Multiple storage specifiers"); diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index 49540b244..46699aaef 100644 --- a/src/frontc/cabsvisit.ml +++ b/src/frontc/cabsvisit.ml @@ -217,7 +217,7 @@ and childrenTypeSpecifier vis ts = and childrenSpecElem (vis: cabsVisitor) (se: spec_elem) : spec_elem = match se with - SpecTypedef | SpecInline | SpecStorage _ | SpecPattern _ -> se + SpecTypedef | SpecInline | SpecStorage _ | SpecPattern _ | SpecNoreturn -> se | SpecCV _ -> se (* cop out *) | SpecAttr a -> begin let al' = visitCabsAttribute vis a in diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll index b4f78fd2a..271f8329f 100644 --- a/src/frontc/clexer.mll +++ b/src/frontc/clexer.mll @@ -163,6 +163,7 @@ let init_lexicon _ = ("inline", fun loc -> INLINE loc); ("__inline", fun loc -> INLINE loc); ("_inline", fun loc -> IDENT ("_inline", loc)); + ("_Noreturn", fun loc -> NORETURN loc); ("__attribute__", fun loc -> ATTRIBUTE loc); ("__attribute", fun loc -> ATTRIBUTE loc); (* diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 5dac0b42c..7a37670f1 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -252,7 +252,7 @@ let transformOffsetOf (speclist, dtype) member = %token EOF %token CHAR INT BOOL DOUBLE FLOAT VOID INT64 INT32 %token INT128 FLOAT128 COMPLEX /* C99 */ -%token GENERIC /* C11 */ +%token GENERIC NORETURN /* C11 */ %token ENUM STRUCT TYPEDEF UNION %token SIGNED UNSIGNED LONG SHORT %token VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER @@ -474,7 +474,7 @@ primary_expression: /*(* 6.5.1. *)*/ ; /* (specifier, expression) list */ -generic_assoc_list: +generic_assoc_list: | generic_association {[$1]} | generic_assoc_list COMMA generic_association {$3 :: $1} @@ -951,6 +951,7 @@ decl_spec_list: /* ISO 6.7 */ | type_spec decl_spec_list_opt_no_named { SpecType (fst $1) :: $2, snd $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) */ diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 3e7b052ef..33d1d11aa 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -135,6 +135,7 @@ let rec print_specifiers (specs: spec_elem list) = let print_spec_elem = function SpecTypedef -> print "typedef" | SpecInline -> printu "inline" + | SpecNoreturn -> printu "_Noreturn" | SpecStorage sto -> printu (match sto with NO_STORAGE -> (comstring "/*no storage*/") @@ -532,11 +533,11 @@ and print_expression_level (lvl: int) (exp : expression) = print ")" | GENERIC (exp, lst) -> let rec print_generic_list l = - match l with + match l with [] -> () | (t, e) :: tl -> print ", "; - print_onlytype t; + print_onlytype t; print ": "; print_expression_level 0 e; print_generic_list tl diff --git a/test/small1/c11-noreturn.c b/test/small1/c11-noreturn.c new file mode 100644 index 000000000..ed9c35d79 --- /dev/null +++ b/test/small1/c11-noreturn.c @@ -0,0 +1,24 @@ +#include "testharness.h" +#include + +_Noreturn int fun() { + return 5; +} + +noreturn int blub() { + return 7; +} + +int blabla() __attribute__((noreturn)); + +int blabla() { + return 8; +} + +int main() { + fun(); + blub(); + blabla(); + + SUCCESS; +} diff --git a/test/small1/gcc-c11-generic-1.c b/test/small1/gcc-c11-generic-1.c index 439ca004b..495ce47d8 100644 --- a/test/small1/gcc-c11-generic-1.c +++ b/test/small1/gcc-c11-generic-1.c @@ -1,7 +1,7 @@ // https://github.com/gcc-mirror/gcc/blob/16e2427f50c208dfe07d07f18009969502c25dc8/gcc/testsuite/gcc.dg/c11-generic-1.c #include "testharness.h" -// _Noreturn extern void abort (void); +_Noreturn extern void abort (void); int e = 0; @@ -50,9 +50,8 @@ main (void) check (n); /* _Noreturn is not part of the function type. */ - // TODO: add back when C11 _Noreturn supported - /* check (_Generic (&abort, void (*) (void): 0, default: n++)); - check (n); */ + check (_Generic (&abort, void (*) (void): 0, default: n++)); + check (n); /* Integer promotions do not occur. */ short s; diff --git a/test/testcil.pl b/test/testcil.pl index 973260756..e71d0bfc3 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -695,6 +695,7 @@ sub addToGroup { addTest("testrunc11/c11-generic"); addTest("testrunc11/c11-caserange"); +addTest("testrunc11/c11-noreturn"); addTest("testrunc11/gcc-c11-generic-1"); # TODO: these messages are not even checked? addTestFail("testc11/gcc-c11-generic-2-1", "Multiple defaults in generic"); From b5f53d6f74223721eaa4b6404e80f1aa042c7508 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 16 Dec 2021 14:25:09 +0100 Subject: [PATCH 2/3] Allow strange corner case arising when including stdnoreturn.h despite using GCC noreturn attribute --- src/frontc/cparser.mly | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 7a37670f1..dee2d2295 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1361,7 +1361,9 @@ pragma: /* (* We want to allow certain strange things that occur in pragmas, so we * cannot use directly the language of expressions *) */ primary_attr: - IDENT { VARIABLE (fst $1) } + IDENT { VARIABLE (fst $1) } + /* (* This is just so code such as __attribute(_NoReturn) is not rejected, which may arise when combining GCC noreturn attribute and including C11 stdnoreturn.h *) */ +| NORETURN { VARIABLE ("__noreturn__") } /*(* The NAMED_TYPE here creates conflicts with IDENT *)*/ | NAMED_TYPE { VARIABLE (fst $1) } | LPAREN attr RPAREN { $2 } From c0868db43a8ff9f1cccdc5bcf9ea5b33db998d18 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 16 Dec 2021 14:54:00 +0100 Subject: [PATCH 3/3] fix so noreturn test actually does not return --- test/small1/c11-noreturn.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/small1/c11-noreturn.c b/test/small1/c11-noreturn.c index ed9c35d79..c05f25591 100644 --- a/test/small1/c11-noreturn.c +++ b/test/small1/c11-noreturn.c @@ -2,17 +2,17 @@ #include _Noreturn int fun() { - return 5; + SUCCESS; } noreturn int blub() { - return 7; + SUCCESS; } int blabla() __attribute__((noreturn)); int blabla() { - return 8; + SUCCESS; } int main() {