From 5a8aac0c27bb67fe7ad6a51db5ee7875d7f9c5f2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 27 Mar 2024 16:25:02 +0100
Subject: [PATCH] [ivette/wp] improve menus
---
ivette/src/frama-c/plugins/wp/index.tsx | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index 07a1a821b7c..f56c222cb59 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -50,12 +50,22 @@ function addStartProofMenus(
): void {
const { marker, kind } = attr;
switch (kind) {
- case 'STMT':
case 'LFUN':
case 'DFUN':
+ menu.push({
+ label: `Prove function using WP`,
+ onClick: () => Server.send(WP.startProofs, marker)
+ });
+ return;
+ case 'STMT':
+ menu.push({
+ label: `Prove statement annotations using WP`,
+ onClick: () => Server.send(WP.startProofs, marker)
+ });
+ return;
case 'PROPERTY':
menu.push({
- label: `Generate WP Goals`,
+ label: `Prove property using WP`,
onClick: () => Server.send(WP.startProofs, marker)
});
return;
--
GitLab