From 6fe7b0ba0234baafb5eecc5886748c6a9585ae3d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 20 Jan 2021 17:52:13 +0100
Subject: [PATCH] [dive] Fixes a crash on functions returning void.
---
src/plugins/dive/build.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 13f3bcbc525..3c7b08f7c2d 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -367,6 +367,7 @@ let build_node_writes context node =
| {skind = Return (Some {enode = Lval lval_res},_)} as return_stmt ->
let callstack = Callstack.push (kf,stmt) callstack in
build_lval_deps callstack return_stmt Data lval_res
+ | {skind = Return (None, _)} -> () (* return void *)
| _ -> assert false (* Cil invariant *)
| exception Kernel_function.No_Statement ->
(* the function is only a prototype *)
--
GitLab