Fix get_stmtLoc for GobView syntactic/semantic search

goblint · Feb 28, 2024 · 02bba93 · 02bba93
1 parent 52b042c
commit 02bba93
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 9 deletions.
diff --git a/src/framework/control.ml b/src/framework/control.ml
@@ -625,13 +625,16 @@ struct
            let node_values = LHT.enum lh |> map (Tuple2.map1 fst) in (* drop context from key *)
            let hashtbl_size = if fast_count node_values then count node_values else 123 in
            let by_loc, by_node = Hashtbl.create hashtbl_size, NodeH.create hashtbl_size in
-           node_values |> iter (fun (node, v) ->
-               let loc = Node.location node in
-               (* join values once for the same location and once for the same node *)
-               let join = Option.some % function None -> v | Some v' -> Spec.D.join v v' in
-               Hashtbl.modify_opt loc join by_loc;
-               NodeH.modify_opt node join by_node;
-             );
+           iter (fun (node, v) ->
+              let loc = match node with
+                | Statement s -> Cil.get_stmtLoc s.skind (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
+                | FunctionEntry _ | Function _ -> Node.location node
+              in
+              (* join values once for the same location and once for the same node *)
+              let join = Option.some % function None -> v | Some v' -> Spec.D.join v v' in
+              Hashtbl.modify_opt loc join by_loc;
+              NodeH.modify_opt node join by_node;
+            ) node_values;
            by_loc, by_node
         in
 

diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml
@@ -68,7 +68,7 @@ struct
         (* Take all statements *)
         |> List.concat_map (fun (f : Cil.fundec) -> f.sallstmts |> List.map (fun s -> f, s))
         (* Add locations *)
-        |> List.map (fun (f, (s : Cil.stmt)) -> (Cilfacade.get_stmtLoc s, f, s))
+        |> List.map (fun (f, (s : Cil.stmt)) -> (Cil.get_stmtLoc s.skind, f, s)) (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
         (* Filter artificial ones by impossible location *)
         |> List.filter (fun ((l : Cil.location), _, _) -> l.line >= 0)
         (* Create hash table *)
@@ -109,7 +109,7 @@ struct
                         fun (s : Cil.stmt) ->
                           succeeding_statement := Some s;
                           (* Evaluate at (directly before) a succeeding location *)
-                          Some(self#try_ask (Cilfacade.get_stmtLoc s) expression)
+                          Some(self#try_ask (Cil.get_stmtLoc s.skind) expression) (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
                       end
                       statement.succs
                 with Not_found -> None