checklink: new disassembler, error severity, ...

- Added the -disass command-line option to disassemble symbols found in
the ELF ;

- Field mismatch now stops the matching of two code fragments, while it
used to only emit an error in the log ;

- Fixed a long-lasting bug in the command-line option ;

- Some error messages have been improved.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1908 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 15 insertions, 0 deletions

diff --git a/checklink/Disassembler.ml b/checklink/Disassembler.ml
new file mode 100644
index 0000000..0e2c688
--- /dev/null
+++ b/checklink/Disassembler.ml
@@ -0,0 +1,15 @@
+open ELF_parsers
+open ELF_types
+open PPC_printers
+open PPC_utils
+
+let disassemble elf sym_name =
+  let sym =
+    List.find
+      (fun sym -> sym.st_name = sym_name)
+      (Array.to_list elf.e_symtab)
+  in
+  match code_of_sym elf sym with
+  | None -> "Couldn't find the code for that symbol name"
+  | Some(ecode) ->
+      string_of_instr_list ecode