summaryrefslogtreecommitdiff
path: root/checklink
diff options
context:
space:
mode:
Diffstat (limited to 'checklink')
-rw-r--r--checklink/Asm_printers.ml8
-rw-r--r--checklink/Check.ml12
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