summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-05-31 08:17:28 +0000
committerGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-05-31 08:17:28 +0000
commit53f005a11435008373bac84362cef8ddd63a4bc0 (patch)
tree67cbdc3837c102f301fed00afb37eb5d18648f0c
parent33041338ca03e3bf4f56dc59a1d38e1b7aa6232c (diff)
checklink: better error messages
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1907 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--checklink/Check.ml19
1 files changed, 10 insertions, 9 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 4de9721..1509343 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -797,7 +797,6 @@ let check_sda ident ofs r addr ffw: f_framework or_err =
program counter [pc].
*)
let rec compare_code ccode ecode pc fw: f_framework or_err =
- let error = ERR("Non-matching instructions") in
match ccode, ecode with
| [], [] -> OK(fw)
| [], e_rest ->
@@ -810,13 +809,12 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
^ rest_str)
| c::cs, e::es ->
let recur_simpl = compare_code cs es (Int32.add 4l pc) in
+ let current_instr =
+ "[" ^ string_of_int32 pc ^ "] " ^ string_of_instruction c ^ " - " ^ string_of_instr e in
+ let error = ERR("Non-matching instructions: " ^ current_instr) in
let fw =
if !debug
- then (
- let curr_instr = " [" ^ string_of_int32 pc ^ "] " ^
- string_of_instruction c ^ " - " ^ string_of_instr e in
- (ff_ef ^%= add_log (DEBUG(curr_instr))) fw
- )
+ then (ff_ef ^%= add_log (DEBUG(current_instr))) fw
else fw
in
match c with
@@ -2533,7 +2531,10 @@ let rec worklist_process (wl: worklist) sfw: s_framework =
sfw
>>> sf_ef ^%=
add_log (ERROR(
- "Unique candidate did not match: " ^ s
+ Printf.sprintf
+ "Unique candidate for %s did not match, reason: %s"
+ name
+ s
))
>>> worklist_process wl
end
@@ -2544,7 +2545,7 @@ let rec worklist_process (wl: worklist) sfw: s_framework =
| [] ->
sfw
>>> sf_ef ^%=
- add_log (ERROR("No matching candidate"))
+ add_log (ERROR("No matching candidate for: " ^ name))
>>> worklist_process wl
| [ffw] ->
worklist_process wl ffw.sf
@@ -2552,7 +2553,7 @@ let rec worklist_process (wl: worklist) sfw: s_framework =
sfw
>>> sf_ef ^%=
add_log (ERROR(
- "Multiple matching candidates for symbol: " ^ name
+ "Multiple matching candidates for: " ^ name
))
>>> worklist_process wl
end