From 331edb4f1ab64c55de952b3a89177f87c838e702 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 12 Jun 2024 11:11:00 +0200
Subject: [PATCH] [Studia] Include global initializations in Ivette's results
Fix #1416
---
src/plugins/studia/studia_request.ml | 32 +++++++++++++++++-----------
1 file changed, 19 insertions(+), 13 deletions(-)
diff --git a/src/plugins/studia/studia_request.ml b/src/plugins/studia/studia_request.ml
index b79ea812ffe..9a82cbe8ea2 100644
--- a/src/plugins/studia/studia_request.ml
+++ b/src/plugins/studia/studia_request.ml
@@ -21,12 +21,14 @@
(**************************************************************************)
open Server
-open Cil_types
let package =
Package.package ~plugin:"studia" ~name:"studia" ~title:"Studia" ()
-type effects = { direct: stmt list; indirect: stmt list }
+type effects = {
+ direct: Printer_tag.localizable list;
+ indirect: Printer_tag.localizable list
+}
let empty = { direct = []; indirect = []; }
@@ -51,26 +53,28 @@ module Effects = struct
let jtype = R.jtype
let to_json effects =
- let markers = Printer_tag.localizable_of_stmt in
R.default |>
- R.set direct (List.map markers effects.direct) |>
- R.set indirect (List.map markers effects.indirect) |>
+ R.set direct effects.direct |>
+ R.set indirect effects.indirect |>
R.to_json
end
+let stmt_marker = Printer_tag.localizable_of_stmt
+let global_marker vi = Printer_tag.localizable_of_declaration (SGlobal vi)
+
let compute_writes zone =
try
let reads = Writes.compute zone in
let add acc = function
| Writes.Assign stmt | CallDirect stmt ->
- { acc with direct = stmt :: acc.direct }
+ { acc with direct = stmt_marker stmt :: acc.direct }
| CallIndirect stmt ->
- { acc with indirect = stmt :: acc.indirect }
+ { acc with indirect = stmt_marker stmt :: acc.indirect }
| FormalInit (_vi, callsites) ->
- let calls = List.flatten (List.map snd callsites) in
- { acc with direct = calls @ acc.direct }
- | GlobalInit (_vi, _initinfo) ->
- acc (* for now ignore global initializations *)
+ let calls = List.concat_map snd callsites in
+ { acc with direct = List.map stmt_marker calls @ acc.direct }
+ | GlobalInit (vi, _initinfo) ->
+ { acc with direct = global_marker vi :: acc.direct }
in
List.fold_left add empty reads
with exn ->
@@ -82,8 +86,10 @@ let compute_reads zone =
try
let reads = Reads.compute zone in
let add acc = function
- | Reads.Direct stmt -> { acc with direct = stmt :: acc.direct }
- | Indirect stmt -> { acc with indirect = stmt :: acc.indirect }
+ | Reads.Direct stmt ->
+ { acc with direct = stmt_marker stmt :: acc.direct }
+ | Indirect stmt ->
+ { acc with indirect = stmt_marker stmt :: acc.indirect }
in
List.fold_left add empty reads
with exn ->
--
GitLab