LinearTwoVarEqualityDomain (goblint.Goblint_lib.LinearTwoVarEqualityDomain)

Abstract states in this domain are represented by structs containing an array and an apron environment. The arrays are modeled as proposed in the paper: Each variable is assigned to an index and each array element represents a linear 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 Rhs : sig ... end

module EqualitiesConjunction : sig ... end

module VarManagement : sig ... end

VarManagement defines the type t of the affine equality domain (a record 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 simplified_monomials_from_texp that converts an apron expression into a list of monomials of reference variables and a constant offset

module ExpressionBounds : 
  SharedFunctions.ConvBounds with type t = VarManagement.t

module D : sig ... end

module D2 : RelationDomain.RD with type var = Apron.Var.t