From dbf04b53b6948f07b1f4b60bdafee09bc818a0b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 30 Nov 2023 17:02:35 +0100
Subject: [PATCH] [ivette/wp] goal's marker
---
ivette/src/frama-c/plugins/wp/api/index.ts | 27 +++++++++++++---------
ivette/src/frama-c/plugins/wp/goals.tsx | 4 ++--
ivette/src/frama-c/plugins/wp/index.tsx | 12 +++-------
ivette/src/frama-c/states.ts | 2 +-
src/plugins/wp/wpApi.ml | 23 ++++++++++++++----
5 files changed, 41 insertions(+), 27 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index 18aff5d59f4..5e73797a2f5 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -181,10 +181,12 @@ export const getAvailableProvers: Server.GetRequest<null,prover[]>= getAvailable
export interface goalsData {
/** Entry identifier. */
wpo: goal;
- /** Property Marker */
- property: marker;
+ /** Associated Marker */
+ marker: marker;
/** Associated declaration, if any */
scope?: decl;
+ /** Property Marker */
+ property: marker;
/** Associated function name, if any */
fct?: string;
/** Associated behavior name, if any */
@@ -211,8 +213,9 @@ export interface goalsData {
export const jGoalsData: Json.Decoder<goalsData> =
Json.jObject({
wpo: jGoal,
- property: jMarker,
+ marker: jMarker,
scope: Json.jOption(jDecl),
+ property: jMarker,
fct: Json.jOption(Json.jString),
bhv: Json.jOption(Json.jString),
thy: Json.jOption(Json.jString),
@@ -228,12 +231,14 @@ export const jGoalsData: Json.Decoder<goalsData> =
/** Natural order for `goalsData` */
export const byGoalsData: Compare.Order<goalsData> =
Compare.byFields
- <{ wpo: goal, property: marker, scope?: decl, fct?: string, bhv?: string,
- thy?: string, name: string, smoke: boolean, passed: boolean,
- status: status, stats: stats, script?: string, saved: boolean }>({
+ <{ wpo: goal, marker: marker, scope?: decl, property: marker,
+ fct?: string, bhv?: string, thy?: string, name: string,
+ smoke: boolean, passed: boolean, status: status, stats: stats,
+ script?: string, saved: boolean }>({
wpo: byGoal,
- property: byMarker,
+ marker: byMarker,
scope: Compare.defined(byDecl),
+ property: byMarker,
fct: Compare.defined(Compare.string),
bhv: Compare.defined(Compare.string),
thy: Compare.defined(Compare.string),
@@ -295,10 +300,10 @@ export const goals: State.Array<goal,goalsData> = goals_internal;
/** Default value for `goalsData` */
export const goalsDataDefault: goalsData =
- { wpo: goalDefault, property: markerDefault, scope: undefined,
- fct: undefined, bhv: undefined, thy: undefined, name: '', smoke: false,
- passed: false, status: statusDefault, stats: statsDefault,
- script: undefined, saved: false };
+ { wpo: goalDefault, marker: markerDefault, scope: undefined,
+ property: markerDefault, fct: undefined, bhv: undefined, thy: undefined,
+ name: '', smoke: false, passed: false, status: statusDefault,
+ stats: statsDefault, script: undefined, saved: false };
/** Proof Server Activity */
export const serverActivity: Server.Signal = {
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index de0453e1c9c..b0d5085ce4b 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -113,8 +113,8 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
const goals = model.getRowCount();
const total = model.getTotalRowCount();
const onSelection = React.useCallback(
- ({ wpo, property }: WP.goalsData) => {
- States.setSelected(property);
+ ({ wpo, marker }: WP.goalsData) => {
+ States.setSelected(marker);
setCurrent(wpo);
}, [setCurrent]);
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index 943e2471d1b..130396a3d38 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -41,9 +41,8 @@ import './style.css';
/* -------------------------------------------------------------------------- */
function WPGoals(): JSX.Element {
- const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped',false);
- const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed',true);
- const [list, flipListView] = Dome.useFlipSettings('frama-c.wp.goals.list',true);
+ const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped');
+ const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed');
const [current, setCurrent] = React.useState(WP.goalDefault);
const scope = States.useCurrentScope();
const [goals, setGoals] = React.useState(0);
@@ -64,14 +63,9 @@ function WPGoals(): JSX.Element {
enabled={hasGoals}
selected={failed}
onClick={flipFailed} />
- <IconButton icon='ITEMS.LIST'
- title='Goals List / Current Goal Details'
- enabled={hasGoals}
- selected={list}
- onClick={flipListView} />
</Ivette.TitleBar>
<GoalTable
- display={list}
+ display={true}
scope={scope}
failed={failed}
current={current}
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index abb59114db2..3e857376950 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -409,7 +409,7 @@ export function reloadArray<K, A>(arr: Array<K, A>): void {
/** Access to Synchronized Array elements. */
export interface ArrayProxy<K, A> {
- model: CompactModel<K,A>;
+ model: CompactModel<K, A>;
length: number;
getData(elt: K | undefined): (A | undefined);
forEach(fn: (row: A, elt: K) => void): void;
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index f25cd68bb03..41b8b9415c0 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -169,6 +169,18 @@ let () = R.register ~package ~kind:`GET ~name:"getAvailableProvers"
let gmodel : Wpo.t S.model = S.model ()
+let get_property g = Printer_tag.PIP (WpPropId.property_of_id g.Wpo.po_pid)
+
+let get_marker g =
+ match g.Wpo.po_formula.source with
+ | Some(stmt,_) -> Printer_tag.localizable_of_stmt stmt
+ | None ->
+ let ip = WpPropId.property_of_id g.Wpo.po_pid in
+ match ip with
+ | IPOther { io_loc = OLStmt(_,stmt) } ->
+ Printer_tag.localizable_of_stmt stmt
+ | _ -> Printer_tag.PIP ip
+
let get_decl g = match g.Wpo.po_idx with
| Function(kf,_) -> Some (Printer_tag.SFunction kf)
| Axiomatic _ -> None (* TODO *)
@@ -191,15 +203,18 @@ let get_status g =
verdict = (ProofEngine.consolidated g).best ;
}
-let () = S.column gmodel ~name:"property"
- ~descr:(Md.plain "Property Marker")
- ~data:(module AST.Marker)
- ~get:(fun g -> Printer_tag.PIP (WpPropId.property_of_id g.Wpo.po_pid))
+let () = S.column gmodel ~name:"marker"
+ ~descr:(Md.plain "Associated Marker")
+ ~data:(module AST.Marker) ~get:get_marker
let () = S.column gmodel ~name:"scope"
~descr:(Md.plain "Associated declaration, if any")
~data:(module D.Joption(AST.Decl)) ~get:get_decl
+let () = S.column gmodel ~name:"property"
+ ~descr:(Md.plain "Property Marker")
+ ~data:(module AST.Marker) ~get:get_property
+
let () = S.option gmodel ~name:"fct"
~descr:(Md.plain "Associated function name, if any")
~data:(module D.Jstring) ~get:get_fct
--
GitLab