[ivette/wp] add menu for generating RTE guards

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',

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                                                     --- */

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                                                     --- *)
 (* -------------------------------------------------------------------------- *)