diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
| commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
| tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /checklink | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Asm_printers.ml | 2 | ||||
| -rw-r--r-- | checklink/Check.ml | 6 | ||||
| -rw-r--r-- | checklink/Fuzz.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index 38a420f6..112c72d0 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -303,7 +303,7 @@ let string_of_instruction = function | Pxoris (i0, i1, c2) -> "Pxoris(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" | Plabel (l0) -> "Plabel(" ^ string_of_label l0 ^ ")" | Pbuiltin (e0, p1, p2) -> "Pbuiltin(" ^ string_of_external_function e0 ^ ", " ^ string_of_list string_of_preg ", " p1 ^ ", " ^ string_of_list string_of_preg ", " p2 ^ ")" -| Pannot (e0, a1) -> +| Pannot (e0, a1) -> let sp_reg_name = string_of_external_function e0 in "Pannot(" ^ string_of_external_function e0 ^ ", " ^ string_of_list (string_of_annot_param sp_reg_name) ", " a1 ^ ")" | Pcfi_adjust n -> "Pcfi_adjust(" ^ string_of_coq_Z n ^ ")" diff --git a/checklink/Check.ml b/checklink/Check.ml index 0e69ab72..b2b9077c 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -421,7 +421,7 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw -> ^ Hashtbl.find ffw.sf.ident_to_name ident) | Csymbol_rel_low (ident, i) | Csymbol_rel_high (ident, i) -> (* should be handled separately in places it occurs *) - ERR("Incorrect reference to far-data symbol " + ERR("Incorrect reference to far-data symbol " ^ Hashtbl.find ffw.sf.ident_to_name ident) let match_z_int32 (cz: Z.t) (ei: int32) = @@ -847,7 +847,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in OK(fw) >>= match_ints 0 bi - >>= lblmap_unify lbl lblvaddr + >>= lblmap_unify lbl lblvaddr >>= match_bools false aa >>= match_bools false lk >>= recur_simpl @@ -1719,7 +1719,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= match_iregs rd rD0 >>= recur_simpl | _ -> error - end + end | Pmfcrbit(rd, bit) -> error | Pmflr(r) -> diff --git a/checklink/Fuzz.ml b/checklink/Fuzz.ml index dc984934..0d091c18 100644 --- a/checklink/Fuzz.ml +++ b/checklink/Fuzz.ml @@ -10,7 +10,7 @@ let string_of_byte = Printf.sprintf "0x%02x" let full_range_of_byte elfmap byte = let byte = Int32.of_int byte in - List.find (fun (a, b, _, _) -> a <= byte && byte <= b) elfmap + List.find (fun (a, b, _, _) -> a <= byte && byte <= b) elfmap let range_of_byte elfmap byte = let (_, _, _, r) = full_range_of_byte elfmap byte in |