From 5b99eec6f36dbac9d59d519cc58ce37dd6251abe Mon Sep 17 00:00:00 2001 From: varobert Date: Thu, 12 Jul 2012 14:57:51 +0000 Subject: checklink: simplifications git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1973 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Frameworks.ml | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) (limited to 'checklink/Frameworks.ml') diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index c448734..92f110c 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -31,20 +31,14 @@ type byte_chunk_desc = 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. *) + via a config file. *) 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) + | Inferred of 'a + | Provided of 'a let from_inferrable = function -| Inferred(x, _) -> x -| Provided(x, _) -> x +| Inferred(x) -> x +| Provided(x) -> x (** This framework is carried along while analyzing the whole ELF file. *) @@ -59,8 +53,9 @@ type e_framework = { chkd_data_syms: bool array; (** 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 inferrable) StringMap.t; + linker script. The set holds conflicts for the mapping, if more than one + mapping is inferred. These are reported once, at the end. *) + section_map: (string inferrable * StringSet.t) StringMap.t; (** We will assign a virtual address to each register that can act as an SDA base register. *) sda_map: (int32 inferrable) IntMap.t; -- cgit v1.2.3