From 3c2ad9e3c3c05a26d0ca343ff9d68966c35685d3 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 27 Mar 2024 16:13:27 +0100
Subject: [PATCH] [ivette/wp] add menu for generating RTE guards
---
ivette/src/frama-c/plugins/wp/api/index.ts | 10 +++++++++
ivette/src/frama-c/plugins/wp/index.tsx | 24 +++++++++++++++++++---
src/plugins/wp/wpApi.ml | 18 ++++++++++++++++
3 files changed, 49 insertions(+), 3 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index a8d5905b164..f6e91065867 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -485,6 +485,16 @@ export const goalsDataDefault: goalsData =
name: '', smoke: false, passed: false, status: statusDefault,
stats: statsDefault, proof: false, script: undefined, saved: false };
+const generateRTEGuards_internal: Server.ExecRequest<marker,null> = {
+ kind: Server.RqKind.EXEC,
+ name: 'plugins.wp.generateRTEGuards',
+ input: jMarker,
+ output: Json.jNull,
+ signals: [],
+};
+/** Generate RTE guards for the function */
+export const generateRTEGuards: Server.ExecRequest<marker,null>= generateRTEGuards_internal;
+
const startProofs_internal: Server.ExecRequest<marker,null> = {
kind: Server.RqKind.EXEC,
name: 'plugins.wp.startProofs',
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index 0c527ec205d..07a1a821b7c 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -41,10 +41,10 @@ import * as WP from 'frama-c/plugins/wp/api';
import './style.css';
/* -------------------------------------------------------------------------- */
-/* --- Generate Goals --- */
+/* --- Context Menus --- */
/* -------------------------------------------------------------------------- */
-function buildMenu(
+function addStartProofMenus(
menu: Dome.PopupMenuItem[],
attr: Ast.markerAttributesData,
): void {
@@ -62,7 +62,25 @@ function buildMenu(
}
}
-ASTview.registerMarkerMenuExtender(buildMenu);
+ASTview.registerMarkerMenuExtender(addStartProofMenus);
+
+function addGenerateRTEGuardsMenu(
+ menu: Dome.PopupMenuItem[],
+ attr: Ast.markerAttributesData,
+): void {
+ const { marker, kind } = attr;
+ switch (kind) {
+ case 'LFUN':
+ case 'DFUN':
+ menu.push({
+ label: `Populate WP RTE guards`,
+ onClick: () => Server.send(WP.generateRTEGuards, marker)
+ });
+ return;
+ }
+}
+
+ASTview.registerMarkerMenuExtender(addGenerateRTEGuardsMenu);
/* -------------------------------------------------------------------------- */
/* --- Goal Component --- */
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index bfa4b231fbc..e6be921ad28 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -381,6 +381,24 @@ let goals =
~add_reload_hook
gmodel
+(* -------------------------------------------------------------------------- *)
+(* --- Generate RTEs --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () =
+ R.register ~package ~kind:`EXEC ~name:"generateRTEGuards"
+ ~descr:(Md.plain "Generate RTE guards for the function")
+ ~input:(module AST.Marker)
+ ~output:(module D.Junit)
+ begin function
+ | PVDecl (Some kf, _, _) ->
+ let setup = Factory.parse (Wp_parameters.Model.get ()) in
+ let driver = Driver.load_driver () in
+ let model = Factory.instance setup driver in
+ WpRTE.generate model kf
+ | _ -> ()
+ end
+
(* -------------------------------------------------------------------------- *)
(* --- Generate goals --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab