Module Bap_wp

module Bil_to_bir : sig ... end

This module provides utilities to translate from a BIL Bil.t expression to a BIR subroutine, for which we can then invoke Precondition.visit_sub to get the weakest precondition.

module Compare : sig ... end
module Constraint : sig ... end

This module implements the abstract data type of constraints which can be used as the input to the Precondition module. These can then be used, e.g. to re-construct the counter-examples found by the verification process.

module Environment : sig ... end

This module represents the environment of a BIR program and is used when determining pre-conditions.

module Loader : sig ... end

This module is used to compute and load intruction properties in order to handle instructions with unknown semantics. It exposes the slots that contain these properties.

module Output : sig ... end

This module exports types and utilities to process and report results found using the WP plugin.

module Precondition : sig ... end

This module exports types and utilities to create preconditions for BIR expressions, blocks and subroutines.

module Ps : sig ... end

A utility for running shell commands.

module Run_parameters : sig ... end

This module contains the parameters the user can set from the command line interface to WP. These flags specify which properties WP should check and updates the default options.

module Runner : sig ... end

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 Symbol : sig ... end

This module exports utility functions for working with the objdump command. It currently uses objdump to get the names of symbols in the .data and .bss sections of a binary and their addresses.

module Utils : sig ... end

This module contains various utility functions.

module Z3_utils : sig ... end

This module exports utility functions for working with Z3. Unfortunately, the module hierarchy necessitates thats some things that might naturally be placed in here have to put elsewhere, in particular any functionality required by Constr or Env.