From 4dabb94737157b7bd581881efc7aa2264d9a87ec Mon Sep 17 00:00:00 2001 From: Valentin Perrelle <valentin.perrelle@cea.fr> Date: Tue, 30 Jun 2020 19:07:36 +0200 Subject: [PATCH] [dive] build scalar nodes for lvalues even if the code is dead --- src/plugins/dive/build.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index 4463838589f..bd8b9d01028 100644 --- a/src/plugins/dive/build.ml +++ b/src/plugins/dive/build.ml @@ -200,12 +200,17 @@ let enumerate_cells ~is_folded_base ~limit lval kinstr = with Abstract_interp.Error_Top -> raise Unknown_location let build_node_kind ~is_folded_base lval kinstr = - match enumerate_cells ~is_folded_base ~limit:1 lval kinstr with - | [node_kind] -> node_kind - | [] (* happens if kinstr is dead code *) -> Scattered (lval, kinstr) - | _ -> assert false - | exception (Too_many_deps _) -> Scattered (lval, kinstr) - | exception Unknown_location -> Unknown (lval, kinstr) + match lval with + | Var vi, offset -> + (* Build a scalar node even if kinstr is dead *) + Scalar (vi, Cil.typeOfLval lval, offset) + | Mem _, _ -> + match enumerate_cells ~is_folded_base ~limit:1 lval kinstr with + | [node_kind] -> node_kind + | [] (* happens if kinstr is dead code *) -> Scattered (lval, kinstr) + | _ -> assert false + | exception (Too_many_deps _) -> Scattered (lval, kinstr) + | exception Unknown_location -> Unknown (lval, kinstr) let default_node_locality callstack = match callstack with -- GitLab