Skip to content

Commit e3cbcf7

Browse files
committed
Fix affeq analysis sparse config param and dune file
1 parent 4176d52 commit e3cbcf7

File tree

4 files changed

+10
-10
lines changed

4 files changed

+10
-10
lines changed

src/analyses/apron/affineEqualityAnalysis.apron.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,15 +14,15 @@ include RelationAnalysis
1414

1515
(* There are two versions of the affeq domain.
1616
1. Sparse without side effects
17-
2. Array with side effects
17+
2. Dense Array with side effects
1818
Default: sparse implementation
19-
The array implementation with side effects of the affeq domain is used when the --enable ana.affeq.side_effects option is set *)
19+
The array implementation with side effects of the affeq domain is used when the --disable ana.affeq.sparse option is set *)
2020
let get_domain: (module RelationDomain.RD) Lazy.t =
2121
lazy (
22-
if GobConfig.get_bool "ana.affeq.side_effects" then
23-
(module AffineEqualityDomainSideEffects.D2 (ArrayVector) (ArrayMatrix))
24-
else
22+
if GobConfig.get_bool "ana.affeq.sparse" then
2523
(module AffineEqualityDomain.D2 (SparseVector) (ListMatrix))
24+
else
25+
(module AffineEqualityDenseDomain.D2 (ArrayVector) (ArrayMatrix))
2626
)
2727

2828
let spec_module: (module MCPSpec) Lazy.t =

src/config/options.schema.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1203,7 +1203,7 @@
12031203
"title": "ana.affeq",
12041204
"type": "object",
12051205
"properties": {
1206-
"side_effects": {
1206+
"sparse": {
12071207
"title": "ana.affeq.sparse",
12081208
"description": "Use sparse implementation of Affine Equality analysis (using lists). If set to false, the dense version is used (using arrays). Default is true (sparse implementation)",
12091209
"type": "boolean",

src/dune

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,9 @@
3535
(apron -> affineEqualityDomain.apron.ml)
3636
(-> affineEqualityDomain.no-apron.ml)
3737
)
38-
(select affineEqualityDomainSideEffects.ml from
39-
(apron -> affineEqualityDomainSideEffects.apron.ml)
40-
(-> affineEqualityDomainSideEffects.no-apron.ml)
38+
(select affineEqualityDenseDomain.ml from
39+
(apron -> affineEqualityDenseDomain.apron.ml)
40+
(-> affineEqualityDenseDomain.no-apron.ml)
4141
)
4242
(select linearTwoVarEqualityAnalysis.ml from
4343
(apron -> linearTwoVarEqualityAnalysis.apron.ml)

src/goblint_lib.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ module ValueDomainQueries = ValueDomainQueries
260260
module RelationDomain = RelationDomain
261261
module ApronDomain = ApronDomain
262262
module AffineEqualityDomain = AffineEqualityDomain
263-
module AffineEqualityDomainSideEffects = AffineEqualityDomainSideEffects
263+
module AffineEqualityDomainDense = AffineEqualityDenseDomain
264264
module LinearTwoVarEqualityDomain = LinearTwoVarEqualityDomain
265265

266266
(** {3 Concurrency} *)

0 commit comments

Comments
 (0)