From 5c5c50482194616040bcd28a0abb8fa03e8f9d39 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 29 Mar 2022 15:58:30 +0200
Subject: [PATCH] [Eva] Values_request: improves [getProbeInfo] request.
---
.../src/frama-c/plugins/eva/api/values/index.ts | 5 +++--
src/plugins/value/api/values_request.ml | 15 +++++++++++----
2 files changed, 14 insertions(+), 6 deletions(-)
diff --git a/ivette/src/frama-c/plugins/eva/api/values/index.ts b/ivette/src/frama-c/plugins/eva/api/values/index.ts
index 4f550b91b0a..c286426c70a 100644
--- a/ivette/src/frama-c/plugins/eva/api/values/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/values/index.ts
@@ -121,7 +121,7 @@ export const getStmtInfo: Server.GetRequest<
const getProbeInfo_internal: Server.GetRequest<
marker,
{ condition: boolean, effects: boolean, rank: number,
- stmt?: Json.key<'#stmt'>, code?: string }
+ stmt?: Json.key<'#stmt'>, code?: string, evaluable: boolean }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getProbeInfo',
@@ -132,6 +132,7 @@ const getProbeInfo_internal: Server.GetRequest<
rank: Json.jFail(Json.jNumber,'Number expected'),
stmt: Json.jKey<'#stmt'>('#stmt'),
code: Json.jString,
+ evaluable: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
signals: [],
};
@@ -139,7 +140,7 @@ const getProbeInfo_internal: Server.GetRequest<
export const getProbeInfo: Server.GetRequest<
marker,
{ condition: boolean, effects: boolean, rank: number,
- stmt?: Json.key<'#stmt'>, code?: string }
+ stmt?: Json.key<'#stmt'>, code?: string, evaluable: boolean }
>= getProbeInfo_internal;
/** Evaluation of an expression or lvalue */
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 05784f500b0..784b1a0fa9a 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -85,10 +85,10 @@ let () = Analysis.register_computation_hook ~on:Computed
let next_steps s =
match s.skind with
| If (cond, _, _, _) -> [ `Then cond ; `Else cond ]
- | Instr (Set _ | Call _ | Local_init _ | Asm _ | Code_annot _)
+ | Instr (Set _ | Call _ | Local_init _) -> [ `After ]
+ | Instr (Asm _ | Code_annot _)
| Switch _ | Loop _ | Block _ | UnspecifiedSequence _
| TryCatch _ | TryFinally _ | TryExcept _
- -> [ `After ]
| Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
let probe_stmt s =
@@ -102,6 +102,7 @@ let probe_stmt s =
let probe marker =
let open Printer_tag in
match marker with
+ | PLval (_, _, (Var vi, NoOffset)) when Cil.isFunctionType vi.vtype -> None
| PLval(_,Kstmt s,l) -> Some (Plval (l,s))
| PExp(_,Kstmt s,e) -> Some (Pexpr (e,s))
| PStmt(_,s) | PStmtStart(_,s) -> probe_stmt s
@@ -530,7 +531,10 @@ let () =
let () =
let getProbeInfo = Request.signature ~input:(module Jmarker) () in
- let set_code = Request.result_opt getProbeInfo
+ let set_evaluable = Request.result getProbeInfo
+ ~name:"evaluable" ~descr:(Md.plain "Can the probe be evaluated?")
+ (module Jbool)
+ and set_code = Request.result_opt getProbeInfo
~name:"code" ~descr:(Md.plain "Probe source code")
(module Jstring)
and set_stmt = Request.result_opt getProbeInfo
@@ -547,6 +551,9 @@ let () =
~default:false (module Jbool)
in
let set_probe rq pp p s =
+ let computed = Analysis.is_computed () in
+ let reachable = Results.is_reachable s in
+ set_evaluable rq (computed && reachable);
set_code rq (Some (Pretty_utils.to_string pp p)) ;
set_stmt rq (Some s) ;
set_rank rq (Ranking.stmt s) ;
@@ -563,7 +570,7 @@ let () =
match probe marker with
| Some (Plval (l, s)) -> set_probe rq Printer.pp_lval l s
| Some (Pexpr (e, s)) -> set_probe rq Printer.pp_exp e s
- | None -> ()
+ | None -> set_evaluable rq false
end
(* -------------------------------------------------------------------------- *)
--
GitLab