summaryrefslogtreecommitdiff
path: root/checklink/Validator.ml
diff options
context:
space:
mode:
authorGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-06-01 13:57:16 +0000
committerGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-06-01 13:57:16 +0000
commit20d10f71ea444e326a7a77670844214375c72514 (patch)
tree35f45c9b96afb13e884aa8f8208c3cb1ef9061e7 /checklink/Validator.ml
parent53f005a11435008373bac84362cef8ddd63a4bc0 (diff)
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
Diffstat (limited to 'checklink/Validator.ml')
-rw-r--r--checklink/Validator.ml22
1 files changed, 19 insertions, 3 deletions
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