diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index f6d7ffc1b679ebb7ff1f5759fdd3b1fbf134f34f..3fa46bf8d2cc5f6db6c93aa124b7be2fdc4fa64c 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -1182,8 +1182,7 @@ decl_spec_wo_type: /* ISO 6.7 */
| REGISTER { SpecStorage REGISTER, $1}
/* ISO 6.7.4 */
| INLINE { SpecInline, $1 }
-| NORETURN { SpecAttr
- (("noreturn",[make_expr $sloc (VARIABLE "c11")])), $1 }
+| NORETURN { SpecAttr (("noreturn",[])), $1 }
| cvspec { $1 }
| attribute_nocv { SpecAttr (fst $1), snd $1 }
;
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 63d023836e1abb370ebdfd7efe7fbd59b931999d..91c4994af7090ed7eaac006847dc3abe015ec2f3 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3750,25 +3750,11 @@ let rec compute_from_root f = function
| _ :: rest -> compute_from_root f rest
-let instrFallsThrough (i : instr) = match i with
- | Local_init _ -> true
- | Set _ -> true
- | Call (None, {enode = Lval (Var e, NoOffset)}, _, _) ->
- (* See if this is exit, or if it has the noreturn attribute *)
- if e.vname = "exit" then false
- else if hasAttribute "noreturn" e.vattr then false
- else true
- | Call _ -> true
- | Asm _ -> true
- | Skip _ -> true
- | Code_annot _ -> true
-
let rec stmtFallsThrough (s: stmt) : bool =
Kernel.debug ~level:4 "stmtFallsThrough stmt %a"
Cil_printer.pp_location (Stmt.loc s);
match s.skind with
- | Instr(il) ->
- instrFallsThrough il
+ | Instr il -> Cil.instr_falls_through il
| UnspecifiedSequence seq ->
blockFallsThrough (block_from_unspecified_sequence seq)
| Return _ | Break _ | Continue _ | Throw _ -> false
@@ -9570,7 +9556,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
!currentFunctionFDEC.svar.vname;
[assert_false ()], res
in
- if not (hasAttribute "noreturn" !currentFunctionFDEC.svar.vattr)
+ if not (typeHasAttribute "noreturn" !currentFunctionFDEC.svar.vtype)
then
!currentFunctionFDEC.sbody.bstmts <-
!currentFunctionFDEC.sbody.bstmts
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 6de7b381b38de52dfc38484f449301ead113812e..d7c54a7de7794c97971f49d2583fb3ab05846771 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -213,17 +213,9 @@ and cfgStmt env (s: stmt) next break cont =
cfgStmt env stmt next break cont
end
in
- let instrFallsThrough (i : instr) : bool = match i with
- Call (_, {enode = Lval (Var vf, NoOffset)}, _, _) ->
- (* See if this has the noreturn attribute *)
- not (hasAttribute "noreturn" vf.vattr)
- | Call (_, f, _, _) ->
- not (typeHasAttribute "noreturn" (typeOf f))
- | _ -> true
- in
match s.skind with
Instr il ->
- if instrFallsThrough il then
+ if Cil.instr_falls_through il then
addOptionSucc next
else
()
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 7187c0295ed8864069b47111d06614c2fa395ed8..20884d33121ce97ec2b1bdb104877647f42d6577 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -245,13 +245,6 @@ let last_loc block =
try f (List.rev block.bstmts)
with Not_found -> unknown_loc
-let has_noreturn_attr = function
- | Call (_, {enode = Lval (Var vf, NoOffset)}, _, _) ->
- Cil.hasAttribute "noreturn" vf.vattr
- | Call (_, f, _, _) ->
- Cil.typeHasAttribute "noreturn" (Cil.typeOf f)
- | _ -> false
-
module LabelMap = struct
include Cil_datatype.Logic_label.Map
let add_builtin name = add (BuiltinLabel name)
@@ -440,9 +433,9 @@ let build_automaton ~annotations kf =
let dest = match stmt.skind with
| Cil_types.Instr instr ->
let dest =
- if has_noreturn_attr instr
- then exit_point
- else control.dest
+ if Cil.instr_falls_through instr
+ then control.dest
+ else exit_point
in
add_edge control.src dest kinstr (Instr (instr, stmt)) loc;
dest
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index b76527a49a7132bbdfcfaca699aa0f47f01aae64..e7e9490e9f02e2e657608401a69878e3d64f99c3 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -569,9 +569,9 @@ let is_in_libc kf =
let has_noreturn_attr kf =
match kf.fundec with
- | Definition ({ svar = { vattr } },_)
- | Declaration (_, { vattr }, _, _) ->
- Cil.hasAttribute "noreturn" vattr
+ | Definition ({ svar = vi },_)
+ | Declaration (_, vi, _, _) ->
+ Cil.typeHasAttribute "noreturn" vi.vtype
let is_first_stmt kf stmt =
try
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c89f78044299d72f91be0c91f4924d4ff75e0faa..31ead251dbcb14e5a00811a67dd84fe604fadf9e 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -722,8 +722,12 @@ class cil_printer () = object (self)
(* variable declaration *)
method vdecl fmt (v:varinfo) =
let stom, rest = Cil.separateStorageModifiers v.vattr in
+ (* Small hack to keep printing noreturn attribute before function type. *)
+ let noreturn_attrs = Cil.(filterAttributes "noreturn" (typeAttr v.vtype)) in
+ let stom_noreturn = stom @ noreturn_attrs in
+ let vtype_no_noreturn = Cil.typeRemoveAttributes ["noreturn"] v.vtype in
let fundecl = if Cil.isFunctionType v.vtype then Some v else None in
- let v = { v with vtype = self#no_ghost_at_first_level v.vtype } in
+ let v = { v with vtype = self#no_ghost_at_first_level vtype_no_noreturn } in
let v =
if v.vformal && not state.print_cil_as_is then begin
match v.vtype with
@@ -744,10 +748,9 @@ class cil_printer () = object (self)
fprintf fmt "%s%a%a%s%a%a"
(if v.vinline then "__inline " else "")
self#storage v.vstorage
- self#attributes stom
- (if stom = [] then "" else " ")
- (self#typ ?fundecl name)
- v.vtype
+ self#attributes stom_noreturn
+ (if stom_noreturn = [] then "" else " ")
+ (self#typ ?fundecl name) v.vtype
self#attributes rest
(*** L-VALUES ***)
@@ -2095,7 +2098,7 @@ class cil_printer () = object (self)
let name' fmt =
if a = [] then pname fmt false
else if nameOpt = None then printAttributes fmt a
- else fprintf fmt "(%a%a)" printAttributes a pname (a <> [])
+ else fprintf fmt "(%a%a)" printAttributes a pname true
in
let partition_ghosts ghost_arg args =
match args with
@@ -2234,9 +2237,6 @@ class cil_printer () = object (self)
not state.print_cil_as_is &&
not (Kernel.is_debug_key_enabled Kernel.dkey_print_bitfields) ->
false
- | "noreturn", [ ACons ("c11",[]) ]
- when not state.print_cil_as_is ->
- fprintf fmt "_Noreturn"; false
| _ -> (* This is the default case *)
(* Add underscores to the name *)
let an' =
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 9d9cfeac0df3a608cf3e335ad8d14109793e37b0..a35aaa54e6cddf0b9a3bf8cbeea3abfc0a423efe 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -425,12 +425,12 @@ let attributeHash: (string, attributeClass) Hashtbl.t =
(* Now come the MSVC declspec attributes *)
List.iter (fun a -> Hashtbl.add table a (AttrName true))
[ "thread"; "naked"; "dllimport"; "dllexport";
- "selectany"; "allocate"; "nothrow"; "novtable"; "property"; "noreturn";
+ "selectany"; "allocate"; "nothrow"; "novtable"; "property";
"uuid"; "align" ];
List.iter (fun a -> Hashtbl.add table a (AttrFunType false))
- [ "format"; "regparm"; "longcall"; "noinline"; "always_inline"; ];
+ [ "format"; "regparm"; "longcall"; "noinline"; "always_inline";];
List.iter (fun a -> Hashtbl.add table a (AttrFunType true))
- [ "stdcall";"cdecl"; "fastcall" ];
+ [ "stdcall";"cdecl"; "fastcall"; "noreturn"];
List.iter (fun a -> Hashtbl.add table a AttrType)
[ "const"; "volatile"; "restrict"; "mode" ];
table
@@ -3232,7 +3232,7 @@ let separateStorageModifiers (al: attribute list) =
let isstoragemod (Attr(an, _) | AttrAnnot an : attribute) : bool =
try
match Hashtbl.find attributeHash an with
- AttrName issm -> issm
+ | AttrName issm -> issm
| _ -> false
with Not_found -> false
in
@@ -5522,6 +5522,10 @@ let has_extern_local_init b =
try fold_local_init b action (); false with Exit -> true
end
+let instr_falls_through = function
+ | Call (_, f, _, _) -> not (typeHasAttribute "noreturn" (typeOf f))
+ | _ -> true
+
let splitFunctionType (ftype: typ)
: typ * (string * typ * attributes) list option * bool * attributes =
match unrollType ftype with
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 8de18151bda5db701e1d4c64d908073119b882b3..a7a2f7f0eaa4b1a98be5b6701bfba2583e1da453 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1320,6 +1320,13 @@ val has_extern_local_init: block -> bool
*)
val is_ghost_else: block -> bool
+val instr_falls_through : instr -> bool
+(** returns [false] if the given instruction is a call to a function with a
+ ["noreturn"] attribute, and [true] otherwise.
+
+ @since Frama-C+dev
+*)
+
(* ************************************************************************* *)
(** {2 Values for manipulating attributes} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index e867089860ec36283d7e7c5b1358126a5d9c975a..0c6abfa91eee04c1aebe5455b06b9903ffebdca2 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -352,16 +352,7 @@ module Base_checker = struct
has successors:@\n%a"
print_stmt stmt Printer.pp_varinfo f.svar
(Pretty_utils.pp_list ~sep:"@\n" print_stmt) stmt.succs
- | Instr(Call (_, called, _, _))
- when Cil.typeHasAttribute "noreturn" (Cil.typeOf called) ->
- if stmt.succs <> [] then
- check_abort
- "exit statement %a in function %a \
- has successors:@\n%a"
- print_stmt stmt Printer.pp_varinfo f.svar
- (Pretty_utils.pp_list ~sep:"@\n" print_stmt) stmt.succs
- | Instr(Call (_, { enode = Lval(Var called,NoOffset)}, _, _))
- when Cil.hasAttribute "noreturn" called.vattr ->
+ | Instr i when not (Cil.instr_falls_through i) ->
if stmt.succs <> [] then
check_abort
"exit statement %a in function %a \
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index f3b8d9158f23ce63b2b85f12d6f53703f6ddec79..a235f02b21d675b3f6fdc259092829b4b98cbcea 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -51,7 +51,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -784,7 +784,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 58862fef58937dbf5328350046f9e835f5142be9..22861bb8b860502478a963a058939debbb3fe233 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -53,7 +53,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void);
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void);
/*@ terminates \false;
exits status: \exit_status == \old(status);
@@ -61,7 +61,7 @@ void __gen_e_acsl_abort(void);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -352,7 +352,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
@@ -375,7 +375,7 @@ void __gen_e_acsl_exit(int status)
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void)
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void)
{
abort();
{
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 72d8735dd4ac5ada3917fd9c83cc0d36d932e785..9c38744e026b52389077dae64f7fe875e17a8dd0 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -45,7 +45,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -765,7 +765,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 4aefe12825df4a78123395e03c8b5f25002e56eb..fbde72d4e6bb3694690b2025904cbcf9a5e49a5f 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -36,7 +36,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void);
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void);
/*@ terminates \false;
exits status: \exit_status == \old(status);
@@ -44,7 +44,7 @@ void __gen_e_acsl_abort(void);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -326,7 +326,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
@@ -349,7 +349,7 @@ void __gen_e_acsl_exit(int status)
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void)
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void)
{
abort();
{
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index a73f89d3e51b69b8b0ed5a264d31391af19baff4..b6071854f7cf43a8065d7089c354f472a5c06b07 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
@@ -133,7 +133,7 @@ void __gen_e_acsl_perror(char const *s);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == 0 || \result == -1;
assigns \result, Frama_C_entropy_source;
@@ -768,7 +768,7 @@ int __gen_e_acsl_usleep(useconds_t usec)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
__e_acsl_store_block((void *)(& status),4UL);
exit(status);
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
index 7583e2dc85f677bd3a25857ec814ec92e0d3f613..2a778a1f8cc1164a0cc0c7124dd2b8fc723976a8 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
@@ -133,7 +133,7 @@ void __gen_e_acsl_perror(char const *s);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == 0 || \result == -1;
assigns \result, Frama_C_entropy_source;
@@ -450,7 +450,7 @@ int __gen_e_acsl_usleep(useconds_t usec)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
__e_acsl_store_block((void *)(& status),4UL);
exit(status);
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index 8aa685ba92e18af0bf58a72afac4562571263bde..ed7d5351a40d9b0e83800814275cc156bb380ccf 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -66,7 +66,7 @@ int __gen_e_acsl_fclose(FILE *stream);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -262,7 +262,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index fed7aed3b602e54e12c844e3bc599200bb7375d3..0fd82086aff53183bb5c5a2f320a2fb4a147469d 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -478,7 +478,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void);
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void);
/*@ terminates \false;
exits status: \exit_status == \old(status);
@@ -486,7 +486,7 @@ void __gen_e_acsl_abort(void);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -1119,7 +1119,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
@@ -1142,7 +1142,7 @@ void __gen_e_acsl_exit(int status)
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void)
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void)
{
abort();
{
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 35f3fda11c223b760e6e8a9d24412ccbe2938594..73499be6d9f9eb8c9661ad73d9c72c4adb6268c9 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -716,7 +716,7 @@ module Computer
Kernel_function.pretty kf;
Dataflow.merge_results ~save_results;
let f = Kernel_function.get_definition kf in
- if Cil.hasAttribute "noreturn" f.svar.vattr && results <> [] then
+ if Cil.typeHasAttribute "noreturn" f.svar.vtype && results <> [] then
Eva_utils.warning_once_current
"function %a may terminate but has the noreturn attribute"
Kernel_function.pretty kf;
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index 45c39bf596948537e69f1d15bac3d9f30ed72505..667f5fe90095a0c20269bb8e1a06a2093bb9e9c0 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -572,7 +572,7 @@ module Make
some warnings are disabled, such as warnings about new garbled mixes. *)
let compute_using_specification ~warn kinstr call spec state =
let vi = Kernel_function.get_vi call.kf in
- if Cil.hasAttribute "noreturn" vi.vattr
+ if Cil.typeHasAttribute "noreturn" vi.vtype
then []
else
(* Initializes the variable returned by the function. *)
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 88b5d0e312385b2f4afe6fa2ea4222bb85bbd803..67ee1541e1c7d78632fa1889de24a777df5c24b3 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -907,7 +907,7 @@ extern __attribute__((__noreturn__)) void __builtin_abort(void);
ensures never_terminates: \false;
assigns \nothing; */
__attribute__((__noreturn__, __FC_BUILTIN__)) void Frama_C_abort(void);
-void Frama_C_abort(void)
+ __attribute__((__noreturn__)) void Frama_C_abort(void)
{
__builtin_abort();
return;
diff --git a/tests/pretty_printing/funptr_noreturn.c b/tests/pretty_printing/funptr_noreturn.c
new file mode 100644
index 0000000000000000000000000000000000000000..d1e5b586f5f39756c3a29da7168fb3703ff1c5ff
--- /dev/null
+++ b/tests/pretty_printing/funptr_noreturn.c
@@ -0,0 +1,24 @@
+/* run.config
+ STDOPT:
+*/
+
+#include <stdlib.h>
+
+__attribute__((__noreturn__)) void f1() {
+ exit(0);
+}
+
+__attribute__((__noreturn__)) void f2(){
+ __attribute__((__noreturn__)) void (*funptr)(void) = &f1;
+ (*funptr)();
+}
+
+_Noreturn void g1() {
+ exit(0);
+}
+
+_Noreturn void g2(){
+ _Noreturn void (*funptr)(void) = &g1;
+ (*funptr)();
+}
+
diff --git a/tests/pretty_printing/oracle/funptr_noreturn.res.oracle b/tests/pretty_printing/oracle/funptr_noreturn.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..365d5165e0af77831dcea9c5551f89b912473fbe
--- /dev/null
+++ b/tests/pretty_printing/oracle/funptr_noreturn.res.oracle
@@ -0,0 +1,71 @@
+[kernel] Parsing funptr_noreturn.c (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdlib.h"
+ __attribute__((__noreturn__)) void f1(void)
+{
+ exit(0);
+ return;
+}
+
+ __attribute__((__noreturn__)) void f2(void)
+{
+ void ( __attribute__((__noreturn__)) (*funptr))(void) = & f1;
+ (*funptr)();
+ return;
+}
+
+ __attribute__((__noreturn__)) void g1(void)
+{
+ exit(0);
+ return;
+}
+
+ __attribute__((__noreturn__)) void g2(void)
+{
+ void ( __attribute__((__noreturn__)) (*funptr))(void) = & g1;
+ (*funptr)();
+ return;
+}
+
+
+[kernel] Parsing ocode_funptr_noreturn.c (with preprocessing)
+[kernel] Parsing funptr_noreturn.c (with preprocessing)
+[kernel] funptr_noreturn.c:7: Warning:
+ def'n of func f1 at funptr_noreturn.c:7 (sum 887) conflicts with the one at ocode_funptr_noreturn.c:4 (sum 1081); keeping the one at ocode_funptr_noreturn.c:4.
+[kernel] funptr_noreturn.c:11: Warning:
+ def'n of func f2 at funptr_noreturn.c:11 (sum 1774) conflicts with the one at ocode_funptr_noreturn.c:10 (sum 1968); keeping the one at ocode_funptr_noreturn.c:10.
+[kernel] funptr_noreturn.c:16: Warning:
+ def'n of func g1 at funptr_noreturn.c:16 (sum 887) conflicts with the one at ocode_funptr_noreturn.c:17 (sum 1081); keeping the one at ocode_funptr_noreturn.c:17.
+[kernel] funptr_noreturn.c:20: Warning:
+ def'n of func g2 at funptr_noreturn.c:20 (sum 1774) conflicts with the one at ocode_funptr_noreturn.c:23 (sum 1968); keeping the one at ocode_funptr_noreturn.c:23.
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdlib.h"
+ __attribute__((__noreturn__)) void f1(void)
+{
+ exit(0);
+ return;
+}
+
+ __attribute__((__noreturn__)) void f2(void)
+{
+ void ( __attribute__((__noreturn__)) (*funptr))(void) = & f1;
+ (*funptr)();
+ return;
+}
+
+ __attribute__((__noreturn__)) void g1(void)
+{
+ exit(0);
+ return;
+}
+
+ __attribute__((__noreturn__)) void g2(void)
+{
+ void ( __attribute__((__noreturn__)) (*funptr))(void) = & g1;
+ (*funptr)();
+ return;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.0.res.oracle b/tests/spec/oracle/default_spec_mode.0.res.oracle
index 06e27d95b3448c17ac6bd3e2344a9d49ee68897d..b3e13b9e5d89582d933fd1ae0127ac058577f079 100644
--- a/tests/spec/oracle/default_spec_mode.0.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -56,8 +56,7 @@ int f4(int *b)
/*@ terminates \false;
exits \false;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/spec/oracle/default_spec_mode.1.res.oracle b/tests/spec/oracle/default_spec_mode.1.res.oracle
index 28bd6a55879c1d62314ef0f7a5f9abe749454cf6..7668bbc5033fcfc662d9bcde65198dcecf365055 100644
--- a/tests/spec/oracle/default_spec_mode.1.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -46,8 +46,7 @@ int f4(int *b)
exits \false;
assigns \nothing;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/spec/oracle/default_spec_mode.2.res.oracle b/tests/spec/oracle/default_spec_mode.2.res.oracle
index a4e0f835c66729e68a1abcef6d843425dc2ec583..b403960922c45df81a872e0f22e4b016b6af6ae9 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -69,8 +69,7 @@ int f4(int *b)
exits \false;
assigns \nothing;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index e1e0f73f9270034131131f5f7ae756e8efd2c9f7..b6067af62b3e8e49e5454106c88617e5f87cd37b 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -71,8 +71,7 @@ int f4(int *b)
exits \false;
assigns \nothing;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/spec/oracle/default_spec_mode.4.res.oracle b/tests/spec/oracle/default_spec_mode.4.res.oracle
index b2591584562925cd8465bd70b86352c20614a251..0822b20709abffb37eac518289366ce12b720f29 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -53,8 +53,7 @@ int f4(int *b)
/*@ terminates \false;
assigns \nothing;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/syntax/oracle/built.res.oracle b/tests/syntax/oracle/built.res.oracle
index c763be7e968b1a58dd56d638d1819526083f6002..5b247f48b47141bf909d042d90b8c4f839d53a60 100644
--- a/tests/syntax/oracle/built.res.oracle
+++ b/tests/syntax/oracle/built.res.oracle
@@ -2,8 +2,8 @@
[kernel] built.i:21:
Case label -1 exceeds range of unsigned int for switch expression. Nothing to worry.
/* Generated by Frama-C */
-__inline static _Noreturn int dummy_f__fc_inline(void);
-__inline static int dummy_f__fc_inline(void)
+__inline static __attribute__((__noreturn__)) int dummy_f__fc_inline
+(void)
{
int __retres;
while (1) ;