From e9559a91edb7273eee51342e2e93cfc9ca53f4e2 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sat, 8 Oct 2022 01:42:05 +0200
Subject: [PATCH] [Dive] Fix a crash when computing dependencies in
Frama_c_show_each calls
---
src/plugins/dive/build.ml | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 8391db176d6..9c984adfd1c 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -513,7 +513,11 @@ let build_node_reads context node =
and build_args_deps callstack zone stmt args callee_kf =
let callstack = Callstack.push (callee_kf,stmt) callstack in
let formals = Kernel_function.get_formals callee_kf in
- List.iter2 (build_arg_dep callstack stmt zone) args formals
+ try
+ List.iter2 (build_arg_dep callstack stmt zone) args formals
+ (* Invalid_argument happens for Frama_C_show_each which does not have
+ any formal but can have any arguments. *)
+ with Invalid_argument _ -> ()
and build_arg_dep callstack stmt zone arg formal =
if exp_contains_read zone stmt arg then
--
GitLab