package sawja

  1. Overview
  2. Docs
package sawja
Legend:
Library
Module
Module type
Parameter
Class
Class type
type condition =
  1. | BinCond of [ `Eq | `Ge | `Gt | `Le | `Lt | `Ne ] * A3Bir.expr * A3Bir.expr
  2. | IsInstanceOf of A3Bir.expr * Javalib_pack.JBasics.object_type
  3. | IsNotInstanceOf of A3Bir.expr * Javalib_pack.JBasics.object_type
  4. | IsArrayElementInstanceOf of A3Bir.expr * A3Bir.expr
  5. | IsNotArrayElementInstanceOf of A3Bir.expr * A3Bir.expr
type formula =
  1. | Atom of condition
  2. | BoolVar of A3Bir.tvar
  3. | And of formula * formula
  4. | Or of formula * formula
type check =
  1. | CheckNullPointer of A3Bir.tvar
  2. | CheckArrayStore of A3Bir.tvar * A3Bir.tvar
  3. | CheckNegativeArraySize of A3Bir.tvar
  4. | CheckCast of A3Bir.tvar * Javalib_pack.JBasics.object_type
  5. | CheckArithmetic of A3Bir.tvar
  6. | CheckArrayLowerBound of A3Bir.tvar * A3Bir.tvar
  7. | CheckArrayUpperBound of A3Bir.tvar * A3Bir.tvar
type should_be_verified =
  1. | False
  2. | ToBeChecked of check
  3. | MethodAssertion of Javalib_pack.JBasics.class_method_signature