type condition = | BinCond of [ `Eq | `Ge | `Gt | `Le | `Lt | `Ne ] * A3Bir.expr * A3Bir.expr| IsInstanceOf of A3Bir.expr * Javalib_pack.JBasics.object_type| IsNotInstanceOf of A3Bir.expr * Javalib_pack.JBasics.object_type| IsArrayElementInstanceOf of A3Bir.expr * A3Bir.expr| IsNotArrayElementInstanceOf of A3Bir.expr * A3Bir.exprtype check = | CheckNullPointer of A3Bir.tvar| CheckArrayStore of A3Bir.tvar * A3Bir.tvar| CheckNegativeArraySize of A3Bir.tvar| CheckCast of A3Bir.tvar * Javalib_pack.JBasics.object_type| CheckArithmetic of A3Bir.tvar| CheckArrayLowerBound of A3Bir.tvar * A3Bir.tvar| CheckArrayUpperBound of A3Bir.tvar * A3Bir.tvartype should_be_verified = | False| ToBeChecked of check| MethodAssertion of Javalib_pack.JBasics.class_method_signature