checklink: improved user-friendliness

Command-line options have been renamed and reordered. Error messages
verbosity is more fine-grained. Possibly spurious debug messages are
more clearly separated from the actual conclusions of the process.

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

5 files changed, 184 insertions, 161 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 3b146b0..6b3653b 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -23,16 +23,20 @@ open Sections
 *)
 let debug = ref false
 
-(** Whether to print the ELF map *)
+(** Whether to print the ELF map. *)
 let print_elfmap = ref false
 
-(** Whether to dump the ELF map *)
+(** Whether to dump the ELF map. *)
 let dump_elfmap = ref false
 
 (** Whether to check that all ELF function/data symbols have been matched
-    against CompCert idents *)
+    against CompCert idents. *)
 let exhaustivity = ref true
 
+(** Whether to print the list of all symbols (function and data) that were not
+    found in .sdump files. *)
+let list_missing = ref false
+
 (** CompCert Asm *)
 type ccode = Asm.instruction list
 
@@ -41,7 +45,7 @@ let print_debug s =
 
 (** Adds a log entry into the framework. *)
 let add_log (entry: log_entry) (efw: e_framework): e_framework =
-  if !debug then print_endline (string_of_log_entry true entry);
+  if !debug then print_endline ("--DEBUG-- " ^ string_of_log_entry true entry);
   {efw with log = entry :: efw.log}
 
 (** [flag] should have only one bit set. *)
@@ -380,12 +384,13 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw ->
   let efw = ffw |. ff_ef in
   match cc with
   | Cint (i) ->
+      let i = z_int32_lax i in
       let msg =
         Printf.sprintf "match_csts Cint %s %s"
-          (string_of_z i)
+          (string_of_int32 i)
           (string_of_int32 ec)
       in
-      check_eq msg ec (z_int32_lax i) ffw
+      check_eq msg ec i ffw
   | Csymbol_low (ident, i) ->
       let candidates =
         try PosMap.find ident sfw.ident_to_sym_ndx
@@ -3315,25 +3320,30 @@ let check_elf_dump elffilename sdumps =
         let symtype = efw.elf.e_symtab.(ndx).st_type in
         symtype = STT_FUNC || symtype = STT_NOTYPE
       )
-      (filter_some
-         (Array.to_list
-            (Array.mapi
-               (fun ndx b -> if b then None else Some(ndx))
-               efw.chkd_fun_syms
-            )
-         )
-      )
+      (list_false_indices efw.chkd_fun_syms)
   in
   if !exhaustivity
   then
     begin match miss_fun with
     | [] -> ()
     | _  ->
-        Printf.printf "%s\n%s\n\n"
-          (string_of_log_entry false
-             (WARNING("the following function symbols do not appear in .sdump files."))
-          )
-          (string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_fun)
+        if !list_missing
+        then
+          Printf.printf "%s\n%s\n"
+            (string_of_log_entry false
+               (WARNING("the following function symbols do not appear in .sdump files."))
+            )
+            (string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_fun)
+        else
+          print_endline
+            (string_of_log_entry false
+               (WARNING(
+                 Printf.sprintf
+                   "%d function symbols do not appear in .sdump files. Add -list-missing to list them."
+                   (List.length miss_fun)
+                )
+               )
+            )
     end
   ;
   (* indicate data symbols that have not been checked *)
@@ -3343,25 +3353,30 @@ let check_elf_dump elffilename sdumps =
         let symtype = efw.elf.e_symtab.(ndx).st_type in
         symtype = STT_OBJECT || symtype = STT_NOTYPE
       )
-      (filter_some
-         (Array.to_list
-            (Array.mapi
-               (fun ndx b -> if b then None else Some(ndx))
-               efw.chkd_data_syms
-            )
-         )
-      )
+      (list_false_indices efw.chkd_data_syms)
   in
   if !exhaustivity
   then
     begin match miss_data with
     | [] -> ()
     | _  ->
-        Printf.printf "%s\n%s\n\n"
-          (string_of_log_entry false
-             (WARNING("the following data symbols do not appear in .sdump files."))
-          )
-          (string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_data)
+        if !list_missing
+        then
+          Printf.printf "%s\n%s\n"
+            (string_of_log_entry false
+               (WARNING("the following data symbols do not appear in .sdump files."))
+            )
+            (string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_data)
+        else
+           print_endline
+            (string_of_log_entry false
+               (WARNING(
+                 Printf.sprintf
+                   "%d data symbols do not appear in .sdump files. Add -list-missing to list them."
+                   (List.length miss_data)
+                )
+               )
+            )
     end
   ;
   (* print diagnosis *)
@@ -3381,14 +3396,14 @@ let check_elf_dump elffilename sdumps =
   in
   begin match worrysome with
   | [] ->
-      Printf.printf "%s\n\n"
+      Printf.printf "%s\n"
         (string_of_log_entry false
            (INFO("Everything seems fine with this ELF."))
         );
       if exists_unknown_chunk
       then
         begin
-          Printf.printf "%s\n\n"
+          Printf.printf "%s\n"
             (string_of_log_entry false
                (INFO("However, some parts of the ELF could not be identified." ^
                         if !print_elfmap
@@ -3399,17 +3414,13 @@ let check_elf_dump elffilename sdumps =
         end
   | _ ->
       if !debug
-      then
-        begin
-          Printf.printf "%s\n\n"
-            (string_of_log_entry false
-               (DEBUG("Final error log:")))
-        end;
+      then Printf.printf "%s\n"
+        (string_of_log_entry true (DEBUG("Final error log:")));
       List.(iter
               (fun e ->
                 match string_of_log_entry false e with
                 | "" -> ()
-                | s -> print_endline s
+                | s -> print_endline (s ^ "scoubidou")
               )
               (rev efw.log)
       )
diff --git a/checklink/ELF_printers.ml b/checklink/ELF_printers.ml
index f0f154e..ffdc414 100644
--- a/checklink/ELF_printers.ml
+++ b/checklink/ELF_printers.ml
@@ -7,145 +7,142 @@ let string_of_elf32_off     = string_of_int32
 let string_of_elf32_word    = string_of_int32
 
 let string_of_elfclass = function
-| ELFCLASSNONE      -> "ELFCLASSNONE"
-| ELFCLASS32        -> "ELFCLASS32"
-| ELFCLASS64        -> "ELFCLASS64"
-| ELFCLASSUNKNOWN   -> "ELFCLASSUNKNOWN"
+| ELFCLASSNONE    -> "ELFCLASSNONE"
+| ELFCLASS32      -> "ELFCLASS32"
+| ELFCLASS64      -> "ELFCLASS64"
+| ELFCLASSUNKNOWN -> "ELFCLASSUNKNOWN"
 
 let string_of_elfdata = function
-| ELFDATANONE       -> "ELFDATANONE"
-| ELFDATA2LSB       -> "ELFDATA2LSB"
-| ELFDATA2MSB       -> "ELFDATA2MSB"
-| ELFDATAUNKNOWN    -> "ELFDATAUNKNOWN"
+| ELFDATANONE    -> "ELFDATANONE"
+| ELFDATA2LSB    -> "ELFDATA2LSB"
+| ELFDATA2MSB    -> "ELFDATA2MSB"
+| ELFDATAUNKNOWN -> "ELFDATAUNKNOWN"
 
 let string_of_ev = function
-| EV_NONE       -> "EV_NONE"
-| EV_CURRENT    -> "EV_CURRENT"
-| EV_UNKNOWN    -> "EV_UNKNOWN"
+| EV_NONE    -> "EV_NONE"
+| EV_CURRENT -> "EV_CURRENT"
+| EV_UNKNOWN -> "EV_UNKNOWN"
 
 let string_of_elf_identification ei =
-  "{\nei_class = " ^ string_of_elfclass ei.ei_class ^
-  ";\nei_data = " ^ string_of_elfdata ei.ei_data ^
+  "{\nei_class   = " ^ string_of_elfclass ei.ei_class ^
+  ";\nei_data    = " ^ string_of_elfdata ei.ei_data ^
   ";\nei_version = " ^ string_of_ev ei.ei_version ^
   ";\n}"
 
 let string_of_et = function
-| ET_NONE       -> "ET_NONE"
-| ET_REL        -> "ET_REL"
-| ET_EXEC       -> "ET_EXEC"
-| ET_DYN        -> "ET_DYN"
-| ET_CORE       -> "ET_CORE"
-| ET_UNKNOWN    -> "ET_UNKNOWN"
+| ET_NONE    -> "ET_NONE"
+| ET_REL     -> "ET_REL"
+| ET_EXEC    -> "ET_EXEC"
+| ET_DYN     -> "ET_DYN"
+| ET_CORE    -> "ET_CORE"
+| ET_UNKNOWN -> "ET_UNKNOWN"
 
 let string_of_em = function
-| EM_NONE           -> "EM_NONE"
-| EM_M32            -> "EM_M32"
-| EM_SPARC          -> "EM_SPARC"
-| EM_386            -> "EM_386"
-| EM_68K            -> "EM_68K"
-| EM_88K            -> "EM_88K"
-| EM_860            -> "EM_860"
-| EM_MIPS           -> "EM_MIPS"
-| EM_MIPS_RS4_BE    -> "EM_MIPS_RS4_BE"
-| EM_PPC            -> "EM_PPC"
-| EM_UNKNOWN        -> "EM_UNKNOWN"
+| EM_NONE        -> "EM_NONE"
+| EM_M32         -> "EM_M32"
+| EM_SPARC       -> "EM_SPARC"
+| EM_386         -> "EM_386"
+| EM_68K         -> "EM_68K"
+| EM_88K         -> "EM_88K"
+| EM_860         -> "EM_860"
+| EM_MIPS        -> "EM_MIPS"
+| EM_MIPS_RS4_BE -> "EM_MIPS_RS4_BE"
+| EM_PPC         -> "EM_PPC"
+| EM_UNKNOWN     -> "EM_UNKNOWN"
 
 let string_of_elf32_ehdr eh =
-  "{\ne_ident       = " ^ string_of_elf_identification  eh.e_ident      ^
-  ";\ne_type        = " ^ string_of_et                  eh.e_type       ^
-  ";\ne_machine     = " ^ string_of_em                  eh.e_machine    ^
-  ";\ne_version     = " ^ string_of_ev                  eh.e_version    ^
-  ";\ne_entry       = " ^ string_of_elf32_addr          eh.e_entry      ^
-  ";\ne_phoff       = " ^ string_of_elf32_off           eh.e_phoff      ^
-  ";\ne_shoff       = " ^ string_of_elf32_off           eh.e_shoff      ^
-  ";\ne_flags       = " ^ string_of_bitstring           eh.e_flags      ^
-  ";\ne_ehsize      = " ^ string_of_elf32_half          eh.e_ehsize     ^
-  ";\ne_phentsize   = " ^ string_of_elf32_half          eh.e_phentsize  ^
-  ";\ne_phnum       = " ^ string_of_elf32_half          eh.e_phnum      ^
-  ";\ne_shentsize   = " ^ string_of_elf32_half          eh.e_shentsize  ^
-  ";\ne_shnum       = " ^ string_of_elf32_half          eh.e_shnum      ^
-  ";\ne_shstrndx    = " ^ string_of_elf32_half          eh.e_shstrndx   ^
+  "{\ne_ident     = " ^ string_of_elf_identification  eh.e_ident      ^
+  ";\ne_type      = " ^ string_of_et                  eh.e_type       ^
+  ";\ne_machine   = " ^ string_of_em                  eh.e_machine    ^
+  ";\ne_version   = " ^ string_of_ev                  eh.e_version    ^
+  ";\ne_entry     = " ^ string_of_elf32_addr          eh.e_entry      ^
+  ";\ne_phoff     = " ^ string_of_elf32_off           eh.e_phoff      ^
+  ";\ne_shoff     = " ^ string_of_elf32_off           eh.e_shoff      ^
+  ";\ne_flags     = " ^ string_of_bitstring           eh.e_flags      ^
+  ";\ne_ehsize    = " ^ string_of_elf32_half          eh.e_ehsize     ^
+  ";\ne_phentsize = " ^ string_of_elf32_half          eh.e_phentsize  ^
+  ";\ne_phnum     = " ^ string_of_elf32_half          eh.e_phnum      ^
+  ";\ne_shentsize = " ^ string_of_elf32_half          eh.e_shentsize  ^
+  ";\ne_shnum     = " ^ string_of_elf32_half          eh.e_shnum      ^
+  ";\ne_shstrndx  = " ^ string_of_elf32_half          eh.e_shstrndx   ^
   ";\n}"
 
 let string_of_sht = function
-| SHT_NULL      -> "SHT_NULL"
-| SHT_PROGBITS  -> "SHT_PROGBITS"
-| SHT_SYMTAB    -> "SHT_SYMTAB"
-| SHT_STRTAB    -> "SHT_STRTAB"
-| SHT_RELA      -> "SHT_RELA"
-| SHT_HASH      -> "SHT_HASH"
-| SHT_DYNAMIC   -> "SHT_DYNAMIC"
-| SHT_NOTE      -> "SHT_NOTE"
-| SHT_NOBITS    -> "SHT_NOBITS"
-| SHT_REL       -> "SHT_REL"
-| SHT_SHLIB     -> "SHT_SHLIB"
-| SHT_DYNSYM    -> "SHT_DYNSYM"
-| SHT_UNKNOWN   -> "SHT_UNKNOWN"
+| SHT_NULL     -> "SHT_NULL"
+| SHT_PROGBITS -> "SHT_PROGBITS"
+| SHT_SYMTAB   -> "SHT_SYMTAB"
+| SHT_STRTAB   -> "SHT_STRTAB"
+| SHT_RELA     -> "SHT_RELA"
+| SHT_HASH     -> "SHT_HASH"
+| SHT_DYNAMIC  -> "SHT_DYNAMIC"
+| SHT_NOTE     -> "SHT_NOTE"
+| SHT_NOBITS   -> "SHT_NOBITS"
+| SHT_REL      -> "SHT_REL"
+| SHT_SHLIB    -> "SHT_SHLIB"
+| SHT_DYNSYM   -> "SHT_DYNSYM"
+| SHT_UNKNOWN  -> "SHT_UNKNOWN"
 
 let string_of_elf32_shdr sh =
-  "{\nsh_name       = " ^ sh.sh_name ^
-  ";\nsh_type       = " ^ string_of_sht         sh.sh_type      ^
-  ";\nsh_flags      = " ^ string_of_elf32_word  sh.sh_flags     ^
-  ";\nsh_addr       = " ^ string_of_elf32_addr  sh.sh_addr      ^
-  ";\nsh_offset     = " ^ string_of_elf32_off   sh.sh_offset    ^
-  ";\nsh_size       = " ^ string_of_elf32_word  sh.sh_size      ^
-  ";\nsh_link       = " ^ string_of_elf32_word  sh.sh_link      ^
-  ";\nsh_info       = " ^ string_of_elf32_word  sh.sh_info      ^
-  ";\nsh_addralign  = " ^ string_of_elf32_word  sh.sh_addralign ^
-  ";\nsh_entsize    = " ^ string_of_elf32_word  sh.sh_entsize   ^
+  "{\nsh_name      = " ^ sh.sh_name ^
+  ";\nsh_type      = " ^ string_of_sht         sh.sh_type      ^
+  ";\nsh_flags     = " ^ string_of_elf32_word  sh.sh_flags     ^
+  ";\nsh_addr      = " ^ string_of_elf32_addr  sh.sh_addr      ^
+  ";\nsh_offset    = " ^ string_of_elf32_off   sh.sh_offset    ^
+  ";\nsh_size      = " ^ string_of_elf32_word  sh.sh_size      ^
+  ";\nsh_link      = " ^ string_of_elf32_word  sh.sh_link      ^
+  ";\nsh_info      = " ^ string_of_elf32_word  sh.sh_info      ^
+  ";\nsh_addralign = " ^ string_of_elf32_word  sh.sh_addralign ^
+  ";\nsh_entsize   = " ^ string_of_elf32_word  sh.sh_entsize   ^
   ";\n}"
 
 let string_of_p_type = function
-| PT_NULL       -> "PT_NULL"
-| PT_LOAD       -> "PT_LOAD"
-| PT_DYNAMIC    -> "PT_DYNAMIC"
-| PT_INTERP     -> "PT_INTERP"
-| PT_NOTE       -> "PT_NOTE"
-| PT_SHLIB      -> "PT_SHLIB"
-| PT_PHDR       -> "PT_PHDR"
-| PT_UNKNOWN    -> "PT_UNKNOWN"
+| PT_NULL    -> "PT_NULL"
+| PT_LOAD    -> "PT_LOAD"
+| PT_DYNAMIC -> "PT_DYNAMIC"
+| PT_INTERP  -> "PT_INTERP"
+| PT_NOTE    -> "PT_NOTE"
+| PT_SHLIB   -> "PT_SHLIB"
+| PT_PHDR    -> "PT_PHDR"
+| PT_UNKNOWN -> "PT_UNKNOWN"
 
 let string_of_elf32_phdr ph =
-  "{\np_type    = " ^ string_of_p_type      ph.p_type   ^
-  ";\np_offset  = " ^ string_of_elf32_off   ph.p_offset ^
-  ";\np_vaddr   = " ^ string_of_elf32_addr  ph.p_vaddr  ^
-  ";\np_paddr   = " ^ string_of_elf32_addr  ph.p_paddr  ^
-  ";\np_filesz  = " ^ string_of_elf32_word  ph.p_filesz ^
-  ";\np_memsz   = " ^ string_of_elf32_word  ph.p_memsz  ^
-  ";\np_flags   = " ^ string_of_bitstring   ph.p_flags  ^
-  ";\np_align   = " ^ string_of_elf32_word  ph.p_align  ^
+  "{\np_type   = " ^ string_of_p_type      ph.p_type   ^
+  ";\np_offset = " ^ string_of_elf32_off   ph.p_offset ^
+  ";\np_vaddr  = " ^ string_of_elf32_addr  ph.p_vaddr  ^
+  ";\np_paddr  = " ^ string_of_elf32_addr  ph.p_paddr  ^
+  ";\np_filesz = " ^ string_of_elf32_word  ph.p_filesz ^
+  ";\np_memsz  = " ^ string_of_elf32_word  ph.p_memsz  ^
+  ";\np_flags  = " ^ string_of_bitstring   ph.p_flags  ^
+  ";\np_align  = " ^ string_of_elf32_word  ph.p_align  ^
   ";\n}"
 
 let string_of_elf32_st_bind = function
-| STB_LOCAL     -> "STB_LOCAL"
-| STB_GLOBAL    -> "STB_GLOBAL"
-| STB_WEAK      -> "STB_WEAK"
-| STB_UNKNOWN   -> "STB_UNKNOWN"
+| STB_LOCAL   -> "STB_LOCAL"
+| STB_GLOBAL  -> "STB_GLOBAL"
+| STB_WEAK    -> "STB_WEAK"
+| STB_UNKNOWN -> "STB_UNKNOWN"
 
 let string_of_elf32_st_type = function
-| STT_NOTYPE    -> "STT_NOTYPE"
-| STT_OBJECT    -> "STT_OBJECT"
-| STT_FUNC      -> "STT_FUNC"
-| STT_SECTION   -> "STT_SECTION"
-| STT_FILE      -> "STT_FILE"
-| STT_UNKNOWN   -> "STT_UNKNOWN"
+| STT_NOTYPE  -> "STT_NOTYPE"
+| STT_OBJECT  -> "STT_OBJECT"
+| STT_FUNC    -> "STT_FUNC"
+| STT_SECTION -> "STT_SECTION"
+| STT_FILE    -> "STT_FILE"
+| STT_UNKNOWN -> "STT_UNKNOWN"
 
 let string_of_elf32_sym s =
-  "{\nst_name   = " ^ s.st_name ^
-  ";\nst_value  = " ^ string_of_elf32_addr      s.st_value  ^
-  ";\nst_size   = " ^ string_of_elf32_word      s.st_size   ^
-  ";\nst_bind   = " ^ string_of_elf32_st_bind   s.st_bind   ^
-  ";\nst_type   = " ^ string_of_elf32_st_type   s.st_type   ^
-  ";\nst_other  = " ^ string_of_int             s.st_other  ^
-  ";\nst_shndx  = " ^ string_of_elf32_half      s.st_shndx  ^
+  "{\nst_name  = " ^ s.st_name ^
+  ";\nst_value = " ^ string_of_elf32_addr      s.st_value  ^
+  ";\nst_size  = " ^ string_of_elf32_word      s.st_size   ^
+  ";\nst_bind  = " ^ string_of_elf32_st_bind   s.st_bind   ^
+  ";\nst_type  = " ^ string_of_elf32_st_type   s.st_type   ^
+  ";\nst_other = " ^ string_of_int             s.st_other  ^
+  ";\nst_shndx = " ^ string_of_elf32_half      s.st_shndx  ^
   ";\n}"
 
 let string_of_elf e =
-  "{\ne_header = " ^ string_of_elf32_ehdr e.e_hdr ^
-  ";\ne_sections = " ^
-  string_of_array string_of_elf32_shdr ",\n" e.e_shdra ^
-  ";\ne_programs = " ^
-  string_of_array string_of_elf32_phdr ",\n" e.e_phdra ^
-  ";\ne_symtab = " ^
-  string_of_array string_of_elf32_sym ",\n" e.e_symtab ^
+  "{\ne_header   = " ^ string_of_elf32_ehdr e.e_hdr ^
+  ";\ne_sections = " ^ string_of_array string_of_elf32_shdr ",\n" e.e_shdra ^
+  ";\ne_programs = " ^ string_of_array string_of_elf32_phdr ",\n" e.e_phdra ^
+  ";\ne_symtab   = " ^ string_of_array string_of_elf32_sym ",\n" e.e_symtab ^
   ";\n}"
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 828299e..72b00b4 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -187,6 +187,8 @@ let string_of_log_entry show_debug entry =
 
 let fatal s = failwith ((format_logtype "FATAL: ") ^ s)
 
+let verbose_elfmap = ref false
+
 let string_of_byte_chunk_desc = function
 | ELF_header -> "ELF header"
 | ELF_progtab -> "ELF program header table"
@@ -202,4 +204,4 @@ let string_of_byte_chunk_desc = function
 | Jumptable -> "Jump table"
 | Float_literal(f) -> "Float literal: " ^ string_of_float f
 | Padding -> "Padding"
-| Unknown(s) -> "   ???   " ^ s
+| Unknown(s) -> "???" ^ (if !verbose_elfmap then s else "")
diff --git a/checklink/Library.ml b/checklink/Library.ml
index ebcbac8..f6b1883 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -161,3 +161,6 @@ let sorted_lookup (compare: 'a -> 'b -> int) (arr: 'a array) (v: 'b): 'a option
       then sorted_lookup_aux i_from (i_mid - 1)
       else Some(arr.(i_mid))
   in sorted_lookup_aux 0 (Array.length arr - 1)
+
+let list_false_indices a =
+  filter_some (Array.(to_list (mapi (fun ndx b -> if b then None else Some(ndx)) a)))
diff --git a/checklink/Validator.ml b/checklink/Validator.ml
index 34c9cbc..1edcdb4 100644
--- a/checklink/Validator.ml
+++ b/checklink/Validator.ml
@@ -23,29 +23,39 @@ let add_disassemble s =
   option_disassemble := true
 
 let options = [
+  (* Main options *)
   "-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)";
+  (* Parsing behavior *)
+  "-relaxed", Arg.Set ELF_parsers.relaxed,
+  "Allows the following behaviors in the ELF parser:
+\t* Use of a fallback heuristic to resolve symbols bootstrapped at load time";
+  (* Printing behavior *)
+  "-no-exhaustive", Arg.Clear Check.exhaustivity,
+  "Disable the exhaustivity check of ELF function and data symbols";
+  "-list-missing", Arg.Set Check.list_missing,
+  "List function and data symbols that were missing in the exhaustivity check";
+  (* Alternative outputs *)
   "-debug", Arg.Set Check.debug,
   "Print a detailed trace of verification";
-  "-noexhaust", Arg.Clear Check.exhaustivity,
-  "Disable the exhaustivity check of ELF function and data symbols";
-  "-printelf", Arg.Set option_printelf,
+  "-disass", Arg.String add_disassemble,
+  "<symname> Disassemble the symbol with specified name (can be repeated)";
+  "-print-elf", Arg.Set option_printelf,
   "Print the contents of the unanalyzed ELF executable";
-  "-printelfmap", Arg.Set Check.print_elfmap,
+  (* ELF map related *)
+  "-print-elfmap", Arg.Set Check.print_elfmap,
   "Print a map of the analyzed ELF executable";
-  "-dumpelfmap", Arg.Set Check.dump_elfmap,
+  "-verbose-elfmap", Arg.Set Frameworks.verbose_elfmap,
+  "Show sections and symbols contained in the unknown parts of the elf map";
+  (* Fuzz testing related *)
+  "-dump-elfmap", Arg.Set Check.dump_elfmap,
   "Dump an ELF map to <exename>.elfmap, for use with random fuzzing";
   "-fuzz", Arg.Set option_fuzz,
   "Random fuzz testing";
-  "-bytefuzz", Arg.Set option_bytefuzz,
+  "-fuzz-byte", Arg.Set option_bytefuzz,
   "Random fuzz testing byte per byte";
-  "-debugfuzz", Arg.Set Fuzz.fuzz_debug,
+  "-fuzz-debug", Arg.Set Fuzz.fuzz_debug,
   "Print a detailed trace of ongoing fuzz testing";
-  "-relaxed", Arg.Set ELF_parsers.relaxed,
-  "Allows the following behaviors in the ELF parser:
-\t* Use of a fallback heuristic to resolve symbols bootstrapped at load time";
 ]
 
 let anonymous arg =