diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts index 8de39b88f57a00eb899e6d2d888e9efefa26b176..b4f1f05f214b589725a73fe5e4860363bee7e051 100644 --- a/ivette/src/frama-c/plugins/wp/api/index.ts +++ b/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 */ diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx index e0956858d832f988166dd2d3a665614062796a48..012d2a881ca07632345dd18fc541f1c0974ec920 100644 --- a/ivette/src/frama-c/plugins/wp/goals.tsx +++ b/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> ); diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml index 61da7c4d7dbda060130b9969d40715e4aa540bf3..0eec40b4198d83eb4fa6fd6888eccedafbc47eca 100644 --- a/src/plugins/wp/wpApi.ml +++ b/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")