Module Bap_wp.Runner

This module is the runner for WP. It will run either a single or comparative analysis based on the number of files inputted by the user.

module Params = Run_parameters
type input = {
program : Bap.Std.program Bap.Std.term;
code_addrs : Utils.Code_addrs.t;
target : Bap_core_theory.Theory.target;
filename : string;
}

The program data.

  • program is the program to be checked.
  • code_addrs is the set of addresses that are known to point to executable code (excludes inlined data in the code sections).
  • target is the target machine.
  • filename is the filename of the program.
val run : Params.t -> input list -> ( Z3.Solver.status, Bap_main.error ) Stdlib.result

run params files ctxt is the main entrypoint for WP. Based on the length of files, it will run either a single or comparative analysis. If 0 or more than 2 files are given, an error is returned. params sets the properties WP will check and update default options.