diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 13f3bcbc5251638fb3fe846bf0642ca4825ce013..3c7b08f7c2d3d75e450d7fd76afdcf0ce8ca1b89 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 *)