package codex

You can search for identifiers within the package.

in-package search v0.2.0

The Codex library for building static analysers based on abstract interpretation

Install

dune-project

Dependency

md5=bc7266a140c6886add673ede90e335d3

sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

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