Module Whilelib.Analysis_sva

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

module Var = While_ast.Var

module Log : Tracelog.S

module SVA_Ival = Single_value_abstraction.Ival

module SVA_Bval = Single_value_abstraction.Quadrivalent

module State : sig ... end

type sva_state = SVA_Ival.integer State.t

val map_pp : (Stdlib.Format.formatter -> 'a State.value -> unit) -> Stdlib.Format.formatter -> 'a State.t -> unit

val state_pp : Stdlib.Format.formatter -> Framac_ival.Ival.t State.t -> unit

val initial_state : unit -> 'a State.t

val expression_sva : sva_state -> While_ast.aexp -> SVA_Ival.integer

val bexpression_sva : sva_state -> While_ast.bexp -> SVA_Bval.boolean

val join : SVA_Ival.Integer_Lattice.t State.t -> SVA_Ival.Integer_Lattice.t State.t -> SVA_Ival.Integer_Lattice.t State.t

val widen : SVA_Ival.Integer_Lattice.t State.t -> SVA_Ival.Integer_Lattice.t State.t -> SVA_Ival.Integer_Lattice.t State.t

val inter : SVA_Ival.Integer_Lattice.t State.t -> SVA_Ival.Integer_Lattice.t State.t -> SVA_Ival.Integer_Lattice.t State.t

val includes : sva_state -> sva_state -> bool

val analyze_stmt : sva_state -> While_ast.stmt -> sva_state

val refine_aexp : sva_state -> While_ast.aexp -> SVA_Ival.integer -> sva_state

val refine_bexp : sva_state -> While_ast.bexp -> SVA_Bval.boolean -> sva_state

val analyze_stmt_refine : sva_state -> While_ast.stmt -> sva_state