From 1b8c864fc7c2f1b3eece5135330904cc867298b9 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 24 Jun 2024 23:04:58 +0200
Subject: [PATCH] [kernel] Handle noreturn attr in Interpreted_automata
---
.../analysis/interpreted_automata.ml | 17 +++++++++++++++--
1 file changed, 15 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 29f82f78abe..6e6d3de14c2 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -245,6 +245,13 @@ 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)
@@ -375,6 +382,7 @@ let build_automaton ~annotations kf =
and return_point = add_vertex () in
let start_code = if annotations then add_vertex () else entry_point in
let end_code = if annotations then add_vertex () else return_point in
+ let exit_point = add_vertex () in
(* AST traversal *)
let rec do_block control kinstr labels block =
@@ -431,8 +439,13 @@ let build_automaton ~annotations kf =
(* Handle statement *)
let dest = match stmt.skind with
| Cil_types.Instr instr ->
- add_edge control.src control.dest kinstr (Instr (instr, stmt)) loc;
- control.dest
+ let dest =
+ if has_noreturn_attr instr
+ then exit_point
+ else control.dest
+ in
+ add_edge control.src dest kinstr (Instr (instr, stmt)) loc;
+ dest
| Cil_types.Return (opt_exp, _) ->
let exited_blocks = Kernel_function.find_all_enclosing_blocks stmt in
--
GitLab