From 82efbf699645a07e2e2a8dda4d2ea3770d5a3641 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 10 Jan 2019 18:05:07 +0100
Subject: [PATCH] [aorai] small fixes after code review
---
src/kernel_internals/parsing/errorloc.mli | 3 ++-
src/plugins/aorai/aorai_graph.ml | 6 +++---
src/plugins/aorai/aorai_metavariables.ml | 4 ++--
src/plugins/aorai/data_for_aorai.ml | 5 ++---
4 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli
index f11792368b9..0089c29d902 100644
--- a/src/kernel_internals/parsing/errorloc.mli
+++ b/src/kernel_internals/parsing/errorloc.mli
@@ -73,7 +73,8 @@ val finishParsing: unit -> unit (** Call this function to finish parsing and
val pp_context_from_file:
?ctx:int -> ?start_line:int -> Format.formatter -> Filepath.position -> unit
-(** prints a readable description of a location *)
+(** prints a readable description of a location
+ @since Frama-C+dev *)
val pp_location: Format.formatter -> Cil_types.location -> unit
(** Parse errors are usually fatal, but their reporting is sometimes
diff --git a/src/plugins/aorai/aorai_graph.ml b/src/plugins/aorai/aorai_graph.ml
index 03cdb1cb3d9..524a66e50af 100644
--- a/src/plugins/aorai/aorai_graph.ml
+++ b/src/plugins/aorai/aorai_graph.ml
@@ -31,8 +31,8 @@ type transition = (typed_condition * action) trans
module Vertex =
struct
type t = state
- let compare x y = x.nums - y.nums
- let hash x = x.nums
+ let compare x y = Pervasives.compare x.nums y.nums
+ let hash x = Hashtbl.hash x.nums
let equal x y = x.nums = y.nums
let default = {
nums = -1; name = ""; multi_state = None;
@@ -43,7 +43,7 @@ end
module Edge =
struct
type t = transition
- let compare x y = x.numt - y.numt
+ let compare x y = Pervasives.compare x.numt y.numt
let default = {
numt = -1; start = Vertex.default; stop = Vertex.default;
cross = TTrue,[]
diff --git a/src/plugins/aorai/aorai_metavariables.ml b/src/plugins/aorai/aorai_metavariables.ml
index 5621752e3f5..a61e5fcb3ac 100644
--- a/src/plugins/aorai/aorai_metavariables.ml
+++ b/src/plugins/aorai/aorai_metavariables.ml
@@ -114,7 +114,7 @@ struct
let diff = Set.diff used initialized in
if not (Set.is_empty diff) then
alarm edge diff;
- (* Add variables intialized by the condition *)
+ (* Add variables initialized by the condition *)
let add_initialized set = function
| Copy_value ((TVar({lv_origin = Some vi}),_),_) -> Set.add vi set
| _ -> set
@@ -132,7 +132,7 @@ let checkInitialization auto =
struct
let is_metavariable vi =
let module Map = Datatype.String.Map in
- Map.exists (fun _ vi' -> (vi'.vid = vi.vid)) auto.metavariables
+ Map.exists (fun _ -> Cil_datatype.Varinfo.equal vi) auto.metavariables
end
in
let module A = InitAnalysis (P) in
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 1c9122c284c..24e1876a48b 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -133,7 +133,7 @@ let rec is_same_expression e1 e2 =
| PVar _,_ | _,PVar _ -> false
| PCst cst1, PCst cst2 -> Logic_utils.is_same_pconstant cst1 cst2
| PCst _,_ | _,PCst _ -> false
- | PPrm (f1,x1), PPrm(f2,x2) -> f1 = x1 && f2 = x2
+ | PPrm (f1,x1), PPrm(f2,x2) -> f1 = f2 && x1 = x2
| PPrm _,_ | _,PPrm _ -> false
| PMetavar x, PMetavar y -> x = y
| PMetavar _,_ | _,PMetavar _ -> false
@@ -1555,8 +1555,7 @@ let setAutomata auto =
let getState num =
List.find (fun st -> st.nums = num) (getAutomata ()).states
-let getStateName num =
- (getState num).name
+let getStateName num = (getState num).name
let getTransition num =
List.find (fun trans -> trans.numt = num) (getAutomata ()).trans
--
GitLab