diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx index 07a1a821b7c4d6ea3308a4794aca175222f3eb07..f56c222cb59c14dff256dd651b4c2ddd2ad09e6c 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;