From 01be9fb1fdeb7c838e8606e9072bfd12fe9c0b4f Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 28 Mar 2023 17:29:15 +0200
Subject: [PATCH] [Dive] Resurect the enum for DiveRange inside
DiveSpecialRange
---
ivette/src/frama-c/plugins/dive/api/index.ts | 36 ++++++++++++++++++--
src/plugins/dive/server_interface.ml | 30 ++++++++++++----
2 files changed, 58 insertions(+), 8 deletions(-)
diff --git a/ivette/src/frama-c/plugins/dive/api/index.ts b/ivette/src/frama-c/plugins/dive/api/index.ts
index 530ef60bda5..a00d03ce47d 100644
--- a/ivette/src/frama-c/plugins/dive/api/index.ts
+++ b/ivette/src/frama-c/plugins/dive/api/index.ts
@@ -286,11 +286,43 @@ const explorationTags_internal: Server.GetRequest<null,tag[]> = {
export const explorationTags: Server.GetRequest<null,tag[]>= explorationTags_internal;
/** A qualitative description of the range of values that this node can take. */
-export type nodeRange = number | string;
+export enum nodeSpecialRange {
+ /** no value ever computed for this node */
+ empty = 'empty',
+ /** this node can only have one value */
+ singleton = 'singleton',
+ /** this node can take almost all values of its type */
+ wide = 'wide',
+}
+
+/** Decoder for `nodeSpecialRange` */
+export const jNodeSpecialRange: Json.Decoder<nodeSpecialRange> =
+ Json.jEnum(nodeSpecialRange);
+
+/** Natural order for `nodeSpecialRange` */
+export const byNodeSpecialRange: Compare.Order<nodeSpecialRange> =
+ Compare.byEnum(nodeSpecialRange);
+
+/** Default value for `nodeSpecialRange` */
+export const nodeSpecialRangeDefault: nodeSpecialRange =
+ nodeSpecialRange.empty;
+
+const nodeSpecialRangeTags_internal: Server.GetRequest<null,tag[]> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.dive.nodeSpecialRangeTags',
+ input: Json.jNull,
+ output: Json.jArray(jTag),
+ signals: [],
+};
+/** Registered tags for the above type. */
+export const nodeSpecialRangeTags: Server.GetRequest<null,tag[]>= nodeSpecialRangeTags_internal;
+
+/** A qualitative or quantitative description of the range of values that this node can take. */
+export type nodeRange = number | nodeSpecialRange;
/** Decoder for `nodeRange` */
export const jNodeRange: Json.Decoder<nodeRange> =
- Json.jUnion<number | string>( Json.jNumber, Json.jString,);
+ Json.jUnion<number | nodeSpecialRange>( Json.jNumber, jNodeSpecialRange,);
/** Natural order for `nodeRange` */
export const byNodeRange: Compare.Order<nodeRange> = Compare.structural;
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index b6b479669f5..3841de7aab8 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -230,17 +230,35 @@ module Computation = struct
include (val publish lookup "exploration" descr)
end
-module NodeRange = struct
- type t = node_range
+module NodeSpecialRange = struct
+ include Enum (struct type t = node_range end)
+
+ let empty = tag "empty" "no value ever computed for this node"
+ let singleton = tag "singleton" "this node can only have one value"
+ let wide = tag "wide" "this node can take almost all values of its type"
+
+ let lookup = function
+ | Empty -> empty
+ | Singleton -> singleton
+ | Wide -> wide
+ | Normal _ -> raise Not_found
+
let descr = "A qualitative description of the range of values \
that this node can take."
- let jtype = declare "nodeRange" ~descr (Junion [ Jnumber ; Jstring ])
+
+ include (val publish lookup "nodeSpecialRange" descr)
+end
+
+module NodeRange = struct
+ type t = node_range
+ let descr = "A qualitative or quantitative description of the range of \
+ values that this node can take."
+ let jtype = declare "nodeRange" ~descr
+ (Junion [ Jnumber ; NodeSpecialRange.jtype ])
let to_json = function
- | Empty -> `String "empty"
- | Singleton -> `String "singleton"
| Normal range_grade -> `Int range_grade
- | Wide -> `String "wide"
+ | range -> NodeSpecialRange.to_json range
let of_json _ = Data.failure "NodeRange.of_json not implemented"
end
--
GitLab