Module Goblint_lib.LinearTwoVarEqualityDomain

OCaml implementation of the linear two-variable equality domain.

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 D : sig ... end
module D2 : RelationDomain.RD with type var = Apron.Var.t