diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx index d2ef458f75c1dba86844b1d374822b1cbc9e91ab..71d7af84859452f94af698093aaf6f98208af8dc 100644 --- a/ivette/src/frama-c/plugins/wp/goals.tsx +++ b/ivette/src/frama-c/plugins/wp/goals.tsx @@ -27,6 +27,17 @@ import { Table, Column } from 'dome/table/views'; import * as States from 'frama-c/states'; import * as WP from 'frama-c/plugins/wp/api'; +/* -------------------------------------------------------------------------- */ +/* --- Scope Column --- */ +/* -------------------------------------------------------------------------- */ + +function getScope(g : WP.goalsData): string { + if (g.bhv && g.fct) return `${g.fct}@{g.bhv}}`; + if (g.fct) return g.fct; + if (g.thy) return g.thy; + return ''; +} + /* -------------------------------------------------------------------------- */ /* --- Status Column --- */ /* -------------------------------------------------------------------------- */ @@ -119,8 +130,13 @@ export function GoalTable(props: GoalTableProps): JSX.Element { onSelection={onWpoSelection} selection={wpoSelection} > - <Column id='name' label='Property' width={200} /> - <Column id='status' label='Status' fill={true} + <Column id='scope' label='Scope' + width={150} + getter={getScope} /> + <Column id='name' label='Property' + width={150} /> + <Column id='status' label='Status' + fill={true} getter={getStatus} render={renderStatus} /> </Table> );