Skip to content

Commit

Permalink
Merge pull request #58 from goblint/c11-noreturn
Browse files Browse the repository at this point in the history
Support for C11 `_Noreturn`
michael-schwarz authored Dec 16, 2021
2 parents c6be79a + c0868db commit 19dd768
Showing 9 changed files with 41 additions and 10 deletions.
1 change: 1 addition & 0 deletions src/frontc/cabs.ml
Original file line number Diff line number Diff line change
@@ -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 *)

1 change: 1 addition & 0 deletions src/frontc/cabs2cil.ml
Original file line number Diff line number Diff line change
@@ -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");
2 changes: 1 addition & 1 deletion src/frontc/cabsvisit.ml
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions src/frontc/clexer.mll
Original file line number Diff line number Diff line change
@@ -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);
(*
9 changes: 6 additions & 3 deletions src/frontc/cparser.mly
Original file line number Diff line number Diff line change
@@ -252,7 +252,7 @@ let transformOffsetOf (speclist, dtype) member =
%token EOF
%token<Cabs.cabsloc> CHAR INT BOOL DOUBLE FLOAT VOID INT64 INT32
%token<Cabs.cabsloc> INT128 FLOAT128 COMPLEX /* C99 */
%token<Cabs.cabsloc> GENERIC /* C11 */
%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
@@ -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) */
@@ -1360,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 }
5 changes: 3 additions & 2 deletions src/frontc/cprint.ml
Original file line number Diff line number Diff line change
@@ -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
24 changes: 24 additions & 0 deletions test/small1/c11-noreturn.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
#include "testharness.h"
#include <stdnoreturn.h>

_Noreturn int fun() {
SUCCESS;
}

noreturn int blub() {
SUCCESS;
}

int blabla() __attribute__((noreturn));

int blabla() {
SUCCESS;
}

int main() {
fun();
blub();
blabla();

SUCCESS;
}
7 changes: 3 additions & 4 deletions test/small1/gcc-c11-generic-1.c
Original file line number Diff line number Diff line change
@@ -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;
1 change: 1 addition & 0 deletions test/testcil.pl
Original file line number Diff line number Diff line change
@@ -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");

0 comments on commit 19dd768

Please sign in to comment.