Sparsification of Affine Equality Matrix

regtest.sh

@@ -14,7 +14,7 @@ if [[ $OSTYPE == 'darwin'* ]]; then
   grep="ggrep"
 fi
 params="`$grep -oP "PARAM: \K.*" $file`"
-cmd="./goblint --enable warn.debug --enable dbg.regression --html $params ${@:3} $file" # -v
+cmd="./goblint --enable warn.debug --enable dbg.regression  $params ${@:3} $file -v" # -v --html 
 echo "$cmd"
 eval $cmd
 echo "See result/index.xml"

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -4,11 +4,17 @@
 
 open Analyses
 
+open ArrayVector
+open ArrayMatrix
+
+open SparseVector
+open ListMatrix
+
 include RelationAnalysis
 
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
-    let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
+    let module AD = AffineEqualityDomain.D2 (SparseVector) (ListMatrix) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct

src/cdomains/affineEquality/abstractMatrix.ml

@@ -0,0 +1,11 @@
+open RatOps
+open AbstractVector
+open Matrix
+
+(** Some functions inside have the suffix _with, which means that the function has side effects. *)
+module type AbstractMatrix =
+  functor (A: RatOps) (V: AbstractVector) ->
+  sig
+    include Matrix with type vec := V(A).t and type num := A.t
+  end
+

src/cdomains/affineEquality/abstractVector.ml

@@ -0,0 +1,10 @@
+open RatOps
+open Vector
+
+(** Some functions inside have the suffix _with, which means that the function has side effects. *)
+module type AbstractVector =
+  functor (A: RatOps) ->
+  sig
+    include Vector with type num:= A.t
+  end
+