Absarray (infer.Biabduction.Absarray)

val array_clean_new_index : bool -> IR.Exp.t -> IR.Exp.t

This function should be used before adding a new index to Earray. The exp is the newly created index. This function "cleans" exp according to whether it is the footprint or current part of the prop. The function faults in the re - execution mode, as an internal check of the tool.

Abstraction for Arrays

val abstract_array_check : 
  IR.Tenv.t ->
  Prop.normal Prop.t ->
  Prop.normal Prop.t

Apply array abstraction and check the result

val array_abstraction_performed : bool IStdlib.IStd.ref

Remember whether array abstraction was performed (to be reset before calling Abs.abstract)

val remove_redundant_elements : 
  IR.Tenv.t ->
  Prop.normal Prop.t ->
  Prop.normal Prop.t

remove redundant elements in an array