Module Options

module Options: sig .. end
General command-line options (globals vars)

General options and types

type mode = private 
| Analyzer
| Simulator
| Disasm
| Trace
| Test
| NoMode
| Serve
Sub components
val check_options : unit -> unit
Check that a file has been set when a mode type needs it
val parse_command_line : unit -> unit
Parse the command line
val command : mode Pervasives.ref
Hold the command select
module ExecFile: sig .. end
Executable file (or unnamed argument)

Static disassembly / Analysis

val get_dba_filename : unit -> string option
val get_dba_configuration_filename : unit -> string option

DBA start address
val get_entry_point : unit -> Bigint.t option
val get_describe_binary : unit -> bool

Disassembly options

val cfgraph : bool Pervasives.ref
Option set to print cfgraph
val decode : bool Pervasives.ref
Option set to only disassemble an opcode
val decode_llvm : bool Pervasives.ref
Option set to only disassemble an opcode to LLVM
val opaque_predicates_file : string Pervasives.ref
Opaque predicate information file (for assisted disassembly)
val violated_call_ret_file : string Pervasives.ref
Call stack tampering information file (for assisted disassembly
val debug_file : string Pervasives.ref
Output debug file
val cfg_file : string Pervasives.ref
Output CFG file

Others stats global vars

val display_statistics : bool Pervasives.ref
val finalsize : int Pervasives.ref
val initsize : int Pervasives.ref
val ftemps : int Pervasives.ref
val itemps : int Pervasives.ref
val fflags : int Pervasives.ref
val iflags : int Pervasives.ref
val nb_refined_lhs : int Pervasives.ref
val nb_equalities_names : int Pervasives.ref
val nb_equalities_classes : int Pervasives.ref
val nb_equalities_refinement : int Pervasives.ref
val nb_nat_predicate_recovery_tries : int Pervasives.ref
val nb_recovered_nat_predicates : int Pervasives.ref
val nb_failed_nat_predicate_recoveries : int Pervasives.ref
val nb_conditional_cache_uses : int Pervasives.ref
val time_nat_flag_recovery : float Pervasives.ref
val time_analysis : float Pervasives.ref
val time_redundant_evals : float Pervasives.ref
val time_equalities : float Pervasives.ref
val time_simpl : float Pervasives.ref
val time_disas : float Pervasives.ref


val nb_workers : int Pervasives.ref
Number of parallel workers
val port : int Pervasives.ref
External port
val backend_port : int Pervasives.ref
Internal port server<->workers
val ip_address : string Pervasives.ref
IP address to listen on

Dynamic analysis


type trace_format = 
| Chunked of Pervasives.in_channel * bool (*
File input channel, either to load it entirely or not
| Stream of string (*
Socket to read trace from
Trace format either a file or network stream
type trace_analysis_config = {
   mutable configuration : Config_piqi.Configuration.t;
   mutable trace_file : string;
   mutable trace_input : trace_format;
Configuration sent to DSE analyses with a configuration, filename, trace_format
val config : trace_analysis_config
Hold the current DSE configuration
val summary_only : bool Pervasives.ref

Formula generation options

val pruning : bool Pervasives.ref
Either to apply the backward pruning phase when generating a formula (default true)
val pol_name : string Pervasives.ref
policy filename when provided on the command line
val natural_cond_enabled : bool Pervasives.ref
Enable lifting low-level condition predicates to higher level predicates on conditional jumps
val flatten_memory : bool Pervasives.ref
Remove the array theory from formula generated. Warning: only works when providing a full concrete memory addressing as concretization policy

Path exploration options

val nth_to_invert : int Pervasives.ref
val nth_alloc : int Pervasives.ref
val nth_free : int Pervasives.ref
val nth_use : int Pervasives.ref
val check_init : bool Pervasives.ref
val bin_to_explore : string Pervasives.ref
val arg_dse : string Pervasives.ref
val config_seed_file : string Pervasives.ref
val strategy : string Pervasives.ref
val trace_limit_length : int Pervasives.ref
val exploration_timeout : float Pervasives.ref
val random_seed : bool Pervasives.ref
val score_file : string Pervasives.ref
val score_alloc : string Pervasives.ref
val score_free : string Pervasives.ref
val score_use : string Pervasives.ref
val l_event : string Pervasives.ref
val dse_trace : string Pervasives.ref
val dse_type : string Pervasives.ref


val experiment : bool Pervasives.ref
Experimental purposes only
module ShareDirectory: sig .. end