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..6038cc494b440117f983034252ebaebde14b2e7b 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -746,8 +746,7 @@ class cil_printer () = object (self)
self#storage v.vstorage
self#attributes stom
(if stom = [] then "" else " ")
- (self#typ ?fundecl name)
- v.vtype
+ (self#typ ?fundecl name) v.vtype
self#attributes rest
(*** L-VALUES ***)
@@ -2095,7 +2094,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
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/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. *)