Module Whilelib.Analysis_svaSource

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

Sourcemodule Var = While_ast.Var
Sourcemodule State : sig ... end
Sourceval map_pp : (Format.formatter -> 'a State.value -> unit) -> Format.formatter -> 'a State.t -> unit
Sourceval initial_state : unit -> 'a State.t
Sourceval bexpression_sva : sva_state -> While_ast.bexp -> SVA_Bval.boolean
Sourceval includes : sva_state -> sva_state -> bool
Sourceval analyze_stmt : sva_state -> While_ast.stmt -> sva_state
Sourceval analyze_stmt_refine : sva_state -> While_ast.stmt -> sva_state