AffineEqualityDomain (goblint.Goblint_lib.AffineEqualityDomain)

Abstract states in the newly added domain are represented by structs containing a matrix and an apron environment. Matrices are modeled as proposed by Karr: Each variable is assigned to a column and each row represents a linear affine relationship that must hold at the corresponding program point. The apron environment is hereby used to organize the order of columns and variables.

module M = Messages

module Mpqf = SharedFunctions.Mpqf

module AffineEqualityMatrix
  (Vec : VectorMatrix.AbstractVector)
  (Mx : VectorMatrix.AbstractMatrix) : 
  sig ... end

module VarManagement
  (Vec : VectorMatrix.AbstractVector)
  (Mx : VectorMatrix.AbstractMatrix) : 
  sig ... end

It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars. Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form.

module ExpressionBounds
  (Vc : VectorMatrix.AbstractVector)
  (Mx : VectorMatrix.AbstractMatrix) : 
  SharedFunctions.ConvBounds with type t = VarManagement(Vc)(Mx).t

As it is specifically used for the new affine equality domain, it can only provide bounds if the expression contains known constants only and in that case, min and max are the same.

module D
  (Vc : VectorMatrix.AbstractVector)
  (Mx : VectorMatrix.AbstractMatrix) : 
  sig ... end

module D2
  (Vc : VectorMatrix.AbstractVector)
  (Mx : VectorMatrix.AbstractMatrix) : 
  RelationDomain.RD with type var = GobApron.Var.t