From 6298431f5c4d0200d826c60b8c8109c6e8c85204 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 Sep 2023 16:01:50 +0200
Subject: [PATCH] [wp/ivette] goals summary

---
 ivette/src/frama-c/plugins/wp/api/index.ts | 12 +++----
 ivette/src/frama-c/plugins/wp/goals.tsx    | 41 ++++++++++++++++++++--
 src/plugins/wp/wpApi.ml                    |  6 ++--
 3 files changed, 48 insertions(+), 11 deletions(-)

diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index d3ea8c14e71..e8bd3107906 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -115,23 +115,23 @@ export const resultDefault: result =
 /** Test Status */
 export type status =
   Json.key<'#NORESULT'> | Json.key<'#COMPUTING'> | Json.key<'#FAILED'> |
-  Json.key<'#STEPOUT'> | Json.key<'#UNKNOWN'> | Json.key<'#PASSED'> |
-  Json.key<'#VALID'> | Json.key<'#INVALID'>;
+  Json.key<'#STEPOUT'> | Json.key<'#UNKNOWN'> | Json.key<'#VALID'> |
+  Json.key<'#PASSED'> | Json.key<'#DOOMED'>;
 
 /** Decoder for `status` */
 export const jStatus: Json.Decoder<status> =
   Json.jUnion<Json.key<'#NORESULT'> | Json.key<'#COMPUTING'> |
               Json.key<'#FAILED'> | Json.key<'#STEPOUT'> |
-              Json.key<'#UNKNOWN'> | Json.key<'#PASSED'> |
-              Json.key<'#VALID'> | Json.key<'#INVALID'>>(
+              Json.key<'#UNKNOWN'> | Json.key<'#VALID'> |
+              Json.key<'#PASSED'> | Json.key<'#DOOMED'>>(
     Json.jKey<'#NORESULT'>('#NORESULT'),
     Json.jKey<'#COMPUTING'>('#COMPUTING'),
     Json.jKey<'#FAILED'>('#FAILED'),
     Json.jKey<'#STEPOUT'>('#STEPOUT'),
     Json.jKey<'#UNKNOWN'>('#UNKNOWN'),
-    Json.jKey<'#PASSED'>('#PASSED'),
     Json.jKey<'#VALID'>('#VALID'),
-    Json.jKey<'#INVALID'>('#INVALID'),
+    Json.jKey<'#PASSED'>('#PASSED'),
+    Json.jKey<'#DOOMED'>('#DOOMED'),
   );
 
 /** Natural order for `status` */
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 0e29a2d0ec9..a02b4300db2 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -21,11 +21,47 @@
 /* ************************************************************************ */
 
 import React from 'react';
+import { IconKind, Cell } from 'dome/controls/labels';
 import { Table, Column } from 'dome/table/views';
 import * as Ivette from 'ivette';
 import * as States from 'frama-c/states';
 import * as WP from 'frama-c/plugins/wp/api';
 
+/* -------------------------------------------------------------------------- */
+/* --- Status Column                                                      --- */
+/* -------------------------------------------------------------------------- */
+
+interface IconStatus {
+  icon: string;
+  kind: IconKind;
+  title: string;
+}
+
+interface Status extends IconStatus { label: string }
+
+const noResult : IconStatus =
+  { icon: 'MINUS', kind: 'disabled', title: 'No Result' };
+
+const baseStatus : { [key:string]: IconStatus } = {
+  'VALID': { icon: 'CHECK', kind: 'positive', title: 'Valid Goal' },
+  'PASSED': { icon: 'CHECK', kind: 'positive', title: 'Passed Test' },
+  'DOOMED': { icon: 'CROSS', kind: 'negative', title: 'Doomed Test' },
+  'FAILED': { icon: 'WARNING', kind: 'negative', title: 'Prover Failure' },
+  'UNKNOWN': { icon: 'ATTENTION', kind: 'warning', title: 'Prover Stucked' },
+  'TIMEOUT': { icon: 'HELP', kind: 'warning', title: 'Prover Timeout' },
+  'STEPOUT': { icon: 'HELP', kind: 'warning', title: 'Prover Stepout' },
+  'COMPUTING': { icon: 'EXECUTE', kind: 'default', title: 'Computing…' },
+};
+
+function getStatus(g : WP.goalsData): Status {
+  const base = baseStatus[g.status] ?? noResult;
+  return { ...base, label: g.stats.summary };
+}
+
+function renderStatus(s : Status): JSX.Element {
+  return <Cell {...s} />;
+}
+
 /* -------------------------------------------------------------------------- */
 /* --- Goals Table                                                        --- */
 /* -------------------------------------------------------------------------- */
@@ -52,8 +88,9 @@ function WPGoals(): JSX.Element {
       onSelection={onWpoSelection}
       selection={wpoSelection}
     >
-      <Column id='status' label='Status' fixed={true} width={80} />
-      <Column id='name' label='Property' />
+      <Column id='name' label='Property' width={200} />
+      <Column id='status' label='Status' fill={true}
+              getter={getStatus} render={renderStatus} />
     </Table>
   );
 }
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index a894d73e80f..95f1c92875a 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -116,14 +116,14 @@ struct
           Jkey "FAILED" ;
           Jkey "STEPOUT" ;
           Jkey "UNKNOWN" ;
-          Jkey "PASSED" ;
           Jkey "VALID" ;
-          Jkey "INVALID" ;
+          Jkey "PASSED" ;
+          Jkey "DOOMED" ;
         ])
   let to_json { smoke ; verdict } =
     `String begin
       match verdict with
-      | VCS.Valid -> if smoke then "INVALID" else "VALID"
+      | VCS.Valid -> if smoke then "DOOMED" else "VALID"
       | VCS.Unknown -> if smoke then "PASSED" else "UNKNOWN"
       | Failed -> "FAILED"
       | NoResult -> "NORESULT"
-- 
GitLab