[ivette/wp] display results

ivette/src/frama-c/plugins/wp/api/index.ts

@@ -163,10 +163,8 @@ export interface goalsData {
   bhv?: string;
   /** Associated axiomatic, if any */
   thy?: string;
-  /** Smoke Test Goal */
-  smoke: boolean;
-  /** Successfull Goal */
-  passed: boolean;
+  /** Smoking (or not) goal and result */
+  result: [ boolean, boolean ];
   /** Verdict Details */
   stats: stats;
   /** Script File */
@@ -184,8 +182,7 @@ export const jGoalsData: Json.Decoder<goalsData> =
     fct: Json.jOption(jFct),
     bhv: Json.jOption(Json.jString),
     thy: Json.jOption(Json.jString),
-    smoke: Json.jBoolean,
-    passed: Json.jBoolean,
+    result: Json.jPair( Json.jBoolean, Json.jBoolean,),
     stats: jStats,
     script: Json.jOption(Json.jString),
     saved: Json.jBoolean,
@@ -195,7 +192,7 @@ export const jGoalsData: Json.Decoder<goalsData> =
 export const byGoalsData: Compare.Order<goalsData> =
   Compare.byFields
     <{ wpo: goal, property: marker, name: string, fct?: fct, bhv?: string,
-       thy?: string, smoke: boolean, passed: boolean, stats: stats,
+       thy?: string, result: [ boolean, boolean ], stats: stats,
        script?: string, saved: boolean }>({
     wpo: byGoal,
     property: byMarker,
@@ -203,8 +200,7 @@ export const byGoalsData: Compare.Order<goalsData> =
     fct: Compare.defined(byFct),
     bhv: Compare.defined(Compare.string),
     thy: Compare.defined(Compare.string),
-    smoke: Compare.boolean,
-    passed: Compare.boolean,
+    result: Compare.pair(Compare.boolean,Compare.boolean,),
     stats: byStats,
     script: Compare.defined(Compare.string),
     saved: Compare.boolean,
@@ -260,7 +256,7 @@ export const goals: State.Array<goal,goalsData> = goals_internal;
 /** Default value for `goalsData` */
 export const goalsDataDefault: goalsData =
   { wpo: goalDefault, property: markerDefault, name: '', fct: undefined,
-    bhv: undefined, thy: undefined, smoke: false, passed: false,
+    bhv: undefined, thy: undefined, result: [ false, false ],
     stats: statsDefault, script: undefined, saved: false };
 
 /** Proof Server Activity */

ivette/src/frama-c/plugins/wp/goals.tsx

@@ -27,11 +27,17 @@ import * as Ivette from 'ivette';
 import * as States from 'frama-c/states';
 import * as WP from 'frama-c/plugins/wp/api';
 
-const renderPassed: Renderer<boolean> =
-  (passed: boolean): JSX.Element =>
+const renderResult: Renderer<[boolean, boolean]> =
+  ([smoking, passed]): JSX.Element =>
   (<Icon
-    id={passed ? 'CIRC.CHECK' : 'CIRC.QUESTION'}
-    fill={passed ? `var(--positive-button-color)` : `var(--negative-button-color)`}
+    id=
+    {passed ? 'CIRC.CHECK' :
+      (smoking ? 'CIRC.CLOSE' : 'CIRC.QUESTION')
+    }
+    fill=
+    {passed ? `var(--positive-button-color)` :
+      (smoking ? `var(--negative-button-color)` : `var(--warning-button-color)`)
+    }
   />);
 
 function WPGoals(): JSX.Element {
@@ -59,9 +65,9 @@ function WPGoals(): JSX.Element {
       <Column id='fct' label='Function' />
       <Column id='name' label='Names' />
       <Column
-        id='passed'
-        label='Success'
-        render={renderPassed}
+        id='result'
+        label='Result'
+        render={renderResult}
       />
     </Table>
   );

src/plugins/wp/wpApi.ml

@@ -185,13 +185,12 @@ let () = S.option gmodel ~name:"thy"
     ~descr:(Md.plain "Associated axiomatic, if any")
     ~data:(module D.Jstring) ~get:get_thy
 
-let () = S.column gmodel ~name:"smoke"
-    ~descr:(Md.plain "Smoke Test Goal")
-    ~data:(module D.Jbool) ~get:Wpo.is_smoke_test
+let get_result g =
+  Wpo.is_smoke_test g, Wpo.is_passed g
 
-let () = S.column gmodel ~name:"passed"
-    ~descr:(Md.plain "Successfull Goal")
-    ~data:(module D.Jbool) ~get:Wpo.is_passed
+let () = S.column gmodel ~name:"result"
+    ~descr:(Md.plain "Smoking (or not) goal and result")
+    ~data:(module D.Jpair (D.Jbool)(D.Jbool)) ~get:get_result
 
 let () = S.column gmodel ~name:"stats"
     ~descr:(Md.plain "Verdict Details")