diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-26 15:46:54 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-26 15:46:54 +0000 |
| commit | ad12162ff1f0d50c43afefc45e1593f27f197402 (patch) | |
| tree | f77430a75e0a4bf12a64b8ee676d40c88ede1041 /checklink | |
| parent | 9fb435abe98f358b1dde5de6604663a176634e53 (diff) | |
Future-proofing: keep signature information in IA32 and PowerPC Asm, just like we already do in ARM Asm.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Asm_printers.ml | 8 | ||||
| -rw-r--r-- | checklink/Check.ml | 12 |
2 files changed, 10 insertions, 10 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index 5b3abe8..c84bd55 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -137,11 +137,11 @@ let string_of_instruction = function | Pandi_ (i0, i1, c2) -> "Pandi_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" | Pandis_ (i0, i1, c2) -> "Pandis_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" | Pb (l0) -> "Pb(" ^ string_of_label l0 ^ ")" -| Pbctr -> "Pbctr" -| Pbctrl -> "Pbctrl" +| Pbctr sg -> "Pbctr" +| Pbctrl sg -> "Pbctrl" | Pbf (c0, l1) -> "Pbf(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" -| Pbl (i0) -> "Pbl(" ^ string_of_ident i0 ^ ")" -| Pbs (i0) -> "Pbs(" ^ string_of_ident i0 ^ ")" +| Pbl (i0, sg) -> "Pbl(" ^ string_of_ident i0 ^ ")" +| Pbs (i0, sg) -> "Pbs(" ^ string_of_ident i0 ^ ")" | Pblr -> "Pblr" | Pbt (c0, l1) -> "Pbt(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" | Pbtbl (i0, l1) -> "Pbtbl(" ^ string_of_ireg i0 ^ ", " ^ string_of_list string_of_label ", " l1 ^ ")" diff --git a/checklink/Check.ml b/checklink/Check.ml index 50928d2..c51e090 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -38,7 +38,7 @@ let exhaustivity = ref true let list_missing = ref false (** CompCert Asm *) -type ccode = Asm.instruction list +type ccode = Asm.coq_function let print_debug s = if !debug then print_endline (string_of_log_entry true (DEBUG(s))) @@ -1021,7 +1021,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pbctr -> + | Pbctr sg -> begin match ecode with | BCCTRx(bo, bi, lk) :: es -> OK(fw) @@ -1031,7 +1031,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pbctrl -> + | Pbctrl sg -> begin match ecode with | BCCTRx(bo, bi, lk) :: es -> OK(fw) @@ -1069,7 +1069,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= compare_code cs es (Int32.add 8l pc) | _ -> error end - | Pbl(ident) -> + | Pbl(ident, sg) -> begin match ecode with | Bx(li, aa, lk) :: es -> let dest = Int32.(add pc (mul 4l (exts li))) in @@ -1090,7 +1090,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pbs(ident) -> + | Pbs(ident, sg) -> begin match ecode with | Bx(li, aa, lk) :: es -> let dest = Int32.(add pc (mul 4l (exts li))) in @@ -2637,7 +2637,7 @@ let rec worklist_process (wl: worklist) sfw: s_framework = label_list = []; } ) - >>> compare_code ccode ecode pc + >>> compare_code ccode.fn_code ecode pc >>^ mark_covered_fun_sym_ndx ndx ) in begin match candidates with |