diff options
Diffstat (limited to 'checklink/Frameworks.ml')
| -rw-r--r-- | checklink/Frameworks.ml | 21 |
1 files changed, 8 insertions, 13 deletions
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; |