Skip to content

Commit 65d0c12

Browse files
CopperCableIsolatorCopperCableIsolator
committed
replaced term "side effects" with alternative description of function behaviour
1 parent 514ffcb commit 65d0c12

File tree

5 files changed

+389
-4
lines changed

5 files changed

+389
-4
lines changed

‎conf.json‎

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
{
2+
"ana": {
3+
"sv-comp": {
4+
"enabled": true,
5+
"functions": true
6+
},
7+
"int": {
8+
"def_exc": true,
9+
"enums": false,
10+
"interval": true
11+
},
12+
"float": {
13+
"interval": true
14+
},
15+
"activated": [
16+
"base",
17+
"threadid",
18+
"threadflag",
19+
"threadreturn",
20+
"mallocWrapper",
21+
"mutexEvents",
22+
"mutex",
23+
"access",
24+
"race",
25+
"escape",
26+
"expRelation",
27+
"mhp",
28+
"assert",
29+
"var_eq",
30+
"symb_locks",
31+
"region",
32+
"thread",
33+
"threadJoins",
34+
"affeq"
35+
],
36+
"path_sens": [
37+
"mutex",
38+
"malloc_null",
39+
"uninit",
40+
"expsplit",
41+
"activeSetjmp",
42+
"memLeak",
43+
"threadflag"
44+
],
45+
"context": {
46+
"widen": false
47+
},
48+
"malloc": {
49+
"wrappers": [
50+
"kmalloc",
51+
"__kmalloc",
52+
"usb_alloc_urb",
53+
"__builtin_alloca",
54+
"kzalloc",
55+
56+
"ldv_malloc",
57+
58+
"kzalloc_node",
59+
"ldv_zalloc",
60+
"kmalloc_array",
61+
"kcalloc",
62+
63+
"ldv_xmalloc",
64+
"ldv_xzalloc",
65+
"ldv_calloc",
66+
"ldv_kzalloc"
67+
]
68+
},
69+
"base": {
70+
"arrays": {
71+
"domain": "partitioned"
72+
}
73+
},
74+
"race": {
75+
"free": false,
76+
"call": false
77+
},
78+
"autotune": {
79+
"enabled": true,
80+
"activated": [
81+
"singleThreaded",
82+
"mallocWrappers",
83+
"noRecursiveIntervals",
84+
"enums",
85+
"congruence",
86+
"wideningThresholds",
87+
"loopUnrollHeuristic",
88+
"memsafetySpecification",
89+
"termination",
90+
"tmpSpecialAnalysis"
91+
]
92+
}
93+
},
94+
"exp": {
95+
"region-offsets": true
96+
},
97+
"solver": "td3",
98+
"sem": {
99+
"unknown_function": {
100+
"spawn": false
101+
},
102+
"int": {
103+
"signed_overflow": "assume_none"
104+
},
105+
"null-pointer": {
106+
"dereference": "assume_none"
107+
}
108+
},
109+
"witness": {
110+
"graphml": {
111+
"enabled": true,
112+
"id": "enumerate",
113+
"unknown": false
114+
},
115+
"yaml": {
116+
"enabled": true,
117+
"format-version": "2.0",
118+
"entry-types": [
119+
"invariant_set"
120+
],
121+
"invariant-types": [
122+
"loop_invariant"
123+
]
124+
},
125+
"invariant": {
126+
"loop-head": true,
127+
"after-lock": false,
128+
"other": false,
129+
"accessed": false,
130+
"exact": true,
131+
"exclude-vars": [
132+
"tmp\\(___[0-9]+\\)?",
133+
"cond",
134+
"RETURN",
135+
"__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
136+
".*____CPAchecker_TMP_[0-9]+",
137+
"__VERIFIER_assert__cond",
138+
"__ksymtab_.*",
139+
"\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
140+
]
141+
}
142+
},
143+
"pre": {
144+
"enabled": false
145+
}
146+
}

‎rref_vec_new_no_filter_baliktad.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Fatal error: exception Sys_error("conf.json: No such file or diretory")

‎src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ sig
3030
val append_matrices: t -> t -> t
3131
end
3232

33-
(** Some functions inside have the suffix _with, which means that the function has side effects. *)
33+
(** Some functions inside have the suffix _with, which means that the function is not purely functional. *)
3434
module type ArrayMatrixFunctor =
3535
functor (A: RatOps) (V: ArrayVectorFunctor) ->
3636
sig
@@ -40,7 +40,8 @@ module type ArrayMatrixFunctor =
4040
(** Array-based matrix implementation.
4141
It provides a normalization function to reduce a matrix into reduced row echelon form.
4242
Operations exploit that the input matrix/matrices are in reduced row echelon form already. *)
43-
(* The functions that have the suffix _with have side effects and were used in a previous version of the affineEqualityDomain.
43+
(* The functions that have the suffix _with are not purely functional and affect the program state beyond their return value.
44+
They were used in a previous version of the affineEqualityDomain.
4445
These calls were removed to transition to list-based matrices.*)
4546
module ArrayMatrix: ArrayMatrixFunctor =
4647
functor (A: RatOps) (V: ArrayVectorFunctor) ->
@@ -180,7 +181,7 @@ module ArrayMatrix: ArrayMatrixFunctor =
180181

181182
let del_cols m cols = timing_wrap "del_cols" (del_cols m) cols
182183

183-
(* This does NOT have the same semantics (minus side effects) as map2i_with. While map2i_with can deal with m and v having different lenghts, map2i will raise Invalid_argument in that case*)
184+
(* This does NOT have the same semantics as map2i_with. While map2i_with can deal with m and v having different lenghts, map2i will raise Invalid_argument in that case*)
184185
let map2i f m v =
185186
let f' x (i,y) = V.to_array @@ f i (V.of_array x) y in
186187
let range_array = Array.init (V.length v) Fun.id in

‎src/cdomains/apron/affineEqualityDomainSideEffects.apron.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
@see <https://doi.org/10.1007/BF00268497> Karr, M. Affine relationships among variables of a program. *)
44

55
(** There are two versions of the AffineEqualityDomain.
6-
This version here is based on side effects, thus it uses Matrix and Vector functions marked with "_with" which use side effects.
6+
This version here is based on a dense implementation that is not purely functional, thus it uses Matrix and Vector functions marked with "_with".
77
Abstract states in the newly added domain are represented by structs containing a matrix and an apron environment.
88
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.
99
The apron environment is hereby used to organize the order of columns and variables. *)

0 commit comments

Comments
 (0)