From 20d10f71ea444e326a7a77670844214375c72514 Mon Sep 17 00:00:00 2001
From: varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 1 Jun 2012 13:57:16 +0000
Subject: 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
---
 checklink/Validator.ml | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

(limited to 'checklink/Validator.ml')

diff --git a/checklink/Validator.ml b/checklink/Validator.ml
index 55e4da1..34c9cbc 100644
--- a/checklink/Validator.ml
+++ b/checklink/Validator.ml
@@ -1,4 +1,5 @@
 open Check
+open Disassembler
 open ELF_parsers
 open ELF_printers
 open Fuzz
@@ -15,9 +16,17 @@ let set_elf_file s =
   | Some _ -> raise (Arg.Bad "multiple ELF executables given on command line")
   end
 
+let option_disassemble = ref false
+let disassemble_list = ref ([]: string list)
+let add_disassemble s =
+  disassemble_list := s :: !disassemble_list;
+  option_disassemble := true
+
 let options = [
-  "-exe <filename>", Arg.String set_elf_file,
-  "Specify the ELF executable file to analyze";
+  "-exe", Arg.String set_elf_file,
+  "<filename> Specify the ELF executable file to analyze";
+  "-disass", Arg.String add_disassemble,
+  "<symname> Disassemble the symbol with specified name (can be repeated)";
   "-debug", Arg.Set Check.debug,
   "Print a detailed trace of verification";
   "-noexhaust", Arg.Clear Check.exhaustivity,
@@ -59,7 +68,14 @@ let _ =
       exit 2
   | Some elffilename ->
       let sdumps = List.rev !sdump_files in
-      if !option_bytefuzz then begin
+      if !option_disassemble then begin
+        let elf = read_elf elffilename in
+        List.iter
+          (fun s ->
+            Printf.printf "Disassembling %s:\n%s\n\n" s (disassemble elf s)
+          )
+          !disassemble_list
+      end else if !option_bytefuzz then begin
         Random.self_init();
         fuzz_every_byte_loop elffilename sdumps
       end else if !option_fuzz then begin
-- 
cgit v1.2.3