From f45af3286a61ceae85160639097da6776ce66098 Mon Sep 17 00:00:00 2001
From: varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 11 Jul 2012 15:04:00 +0000
Subject: checklink: added configurability

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1969 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Frameworks.ml | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

(limited to 'checklink/Frameworks.ml')

diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 72b00b4..a35537c 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -28,6 +28,24 @@ type byte_chunk_desc =
   | Padding
   | Unknown            of string
 
+let add_uniq x l = if List.mem x l then l else x :: l
+
+(* This type specifies whether its argument was inferred by the tool or provided
+   via a config file, and lists the conflicts that were detected by the tool in
+   the right component of the pair. This allows us to report every conflict once
+   rather than at every occurence of a conflict. *)
+type 'a inferrable =
+  | Inferred of 'a * 'a list
+  | Provided of 'a * 'a list
+
+let add_failure failure = function
+| Inferred(x, failures) -> Inferred(x, add_uniq failure failures)
+| Provided(x, failures) -> Provided(x, add_uniq failure failures)
+
+let from_inferrable = function
+| Inferred(x, _) -> x
+| Provided(x, _) -> x
+
 (** This framework is carried along while analyzing the whole ELF file.
 *)
 type e_framework = {
@@ -42,10 +60,10 @@ type e_framework = {
   (** The mapping from CompCert sections to ELF sections will be inferred along
       the way. This way, we can check things without prior knowledge of the
       linker script. *)
-  section_map: string StringMap.t;
+  section_map: (string inferrable) StringMap.t;
   (** We will assign a virtual address to each register that can act as an SDA
       base register. *)
-  sda_map: int32 IntMap.t;
+  sda_map: (int32 inferrable) IntMap.t;
 }
 
 module PosOT = struct
-- 
cgit v1.2.3