package codex

You can search for identifiers within the package.

in-package search v0.2.0

Module `Whilelib.Analysis_sva`Source

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 Log : Tracelog.S

Sourcemodule SVA_Ival = Single_value_abstraction.Ival

Sourcemodule SVA_Bval = Single_value_abstraction.Quadrivalent

Sourcemodule State : sig ... end

Sourcetype sva_state = SVA_Ival.integer State.t

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

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

Sourceval initial_state : unit -> 'a State.t

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

Sourceval 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

Sourceval includes : sva_state -> sva_state -> bool

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

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

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

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