Module Whilelib.While_analysisSource

This module presents the implementation of a simple example analyzer for the while language using codex constructs. It is detailed in the While tutorial's chapter4.

Sourcemodule Terms : sig ... end
module NonRelationalDomain : sig ... end
Sourcemodule Domain : sig ... end
Sourcemodule Var = While_ast.Var
Sourcetype state = {
  1. ctx : Domain.Context.t;
  2. store : Domain.integer Store.t;
}
Sourceval initial_state : unit -> state
Sourceval pp : Format.formatter -> state -> unit
Sourceval join : state -> state -> state
Sourceval join_opt : state option -> state option -> state option
Sourceval widen : int -> state -> state -> state * bool
Sourceval pp_ret : Format.formatter -> state option -> unit
Sourceval copy : state -> state
Sourceval (let*) : 'a option -> ('a -> 'b option) -> 'b option
Sourceval analyze_stmt : state option -> While_ast.stmt -> state option