Run_parameters (bap_wp.Bap_wp.Run

module Env = Environment

module Err : 
  Monads.Std.Monad.Result.S
    with type 'a t :=
           'a
             Monads.Std.Monad.Result.T1(Bap_main.Extension.Error)(Monads.Std.Monad.Ident).t
     and type 'a m :=
           'a
             Monads.Std.Monad.Result.T1(Bap_main.Extension.Error)(Monads.Std.Monad.Ident).m
     and type 'a e :=
           'a
             Monads.Std.Monad.Result.T1(Bap_main.Extension.Error)(Monads.Std.Monad.Ident).e
     and type err := Bap_main.Extension.Error.t

A result monad that includes Extension.Error.t as the error type. This error is returned when a user passes in an invalid parameter.

type t = {

func : string;

precond : string;

postcond : string;

trip_asserts : bool;

check_null_derefs : bool;

check_invalid_derefs : bool;

compare_func_calls : bool;

compare_post_reg_values : string list;

pointer_reg_list : string list;

inline : string option;

num_unroll : int option;

loop_invariant : string;

gdb_output : string option;

bildb_output : string option;

use_fun_input_regs : bool;

mem_offset : bool;

rewrite_addresses : bool;

debug : string list;

stack_base : int option;

stack_size : int option;

show : string list;

func_name_map : (string * string) list;

user_func_specs : (string * string * string) list;

user_func_specs_orig : (string * string * string) list;

user_func_specs_mod : (string * string * string) list;

fun_specs : string list;

ogre : string option;

ogre_orig : string option;

ogre_mod : string option;

ext_solver_path : string option;

init_mem : bool;

}

The available options to be set. Each flag corresponds to a parameter in the set with the BAP custom command line.

val validate : t -> string list -> ( t, Bap_main.error ) Stdlib.result

validate flags files ensures the user inputted the appropriate flags for the inputted files. In the case the user has invalid flags, an error is returned.

val validate_func : string -> ( unit, Bap_main.error ) Stdlib.result

validate_func name checks the user inputted a name for the function to analyze. Returns an error when name is empty.

val validate_debug : string list -> ( unit, Bap_main.error ) Stdlib.result

validate_debug options checks the user inputted the supported options for the debug printer flag. Returns an error when an unsupported option is inputted.

val validate_show : string list -> ( unit, Bap_main.error ) Stdlib.result

validate_show options checks the user inputted the supported options for the show printer flag. Returns an error when an unsupported option is inputted.

val validate_compare_func_calls : 
  bool ->
  string list ->
  ( unit, Bap_main.error ) Stdlib.result

validate_compare_func_calls flag files checks that the flag is only set when there are two files to compare. Returns an error otherwise.

val validate_compare_post_reg_vals : 
  string list ->
  string list ->
  ( unit, Bap_main.error ) Stdlib.result

validate_compare_post_reg_vals regs files checks that the list of registers to compare is only set when there are two files to compare. Returns an error otherwise.

val validate_mem_flags : 
  t ->
  string list ->
  ( unit, Bap_main.error ) Stdlib.result

validate_mem_flags flags files checks that a memory comparison flag is only set when there are two files to compare, and that only one flag is set at a time. Returns an error otherwise.

val validate_check_invalid_derefs : 
  bool ->
  string list ->
  ( unit, Bap_main.error ) Stdlib.result

validate_check_invalid_derefs flag files checks that the flag is only set when there are two files to compare. Returns an error otherwise.

val validate_ogre : t -> ( t, Bap_main.error ) Stdlib.result

validate_ogre flags checks that the user hasn't provided inconsistent info about which ogre files to use, and updates them with explicit paths if needed. Returns an error otherwise.

val parse_loop_invariant : 
  string ->
  Bap_core_theory.Theory.target ->
  Bap.Std.Sub.t ->
  Env.loop_invariants

parse_loop_environment invariant target sub parses the invariant which is an S-expression representing the address of a loop header and its corresponding loop invariant, and returns a format accepted by the environment.

i.e., parse_loop_environment "(((address 0x12) (invariant "(assert (= foo bar))")))" x86 sub.

val default : func:string -> t

Creates the default parameters for easy invocation