Skip to content

Commit 814997a

Browse files
sim642sim642
committed
Merge branch 'master' into traces-vojdani
2 parents 1e70e33 + 9a8dd4e commit 814997a

File tree

307 files changed

+4227
-2482
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

307 files changed

+4227
-2482
lines changed

‎.github/workflows/coverage.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ jobs:
1616
fail-fast: false
1717
matrix:
1818
os:
19-
- ubuntu-latest
19+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
2020
ocaml-compiler:
2121
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
2222
# don't add any other because they won't be used
@@ -40,7 +40,7 @@ jobs:
4040
ocaml-compiler: ${{ matrix.ocaml-compiler }}
4141

4242
- name: Install graph-easy # TODO: remove if depext --with-test works
43-
if: ${{ matrix.os == 'ubuntu-latest' }}
43+
if: ${{ matrix.os == 'ubuntu-22.04' }}
4444
run: sudo apt install -y libgraph-easy-perl
4545

4646
- name: Install dependencies

‎.github/workflows/docs.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ jobs:
1616
strategy:
1717
matrix:
1818
os:
19-
- ubuntu-latest
19+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
2020
ocaml-compiler:
2121
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
2222
# don't add any other because they won't be used

‎.github/workflows/indentation.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ jobs:
1010
strategy:
1111
matrix:
1212
os:
13-
- ubuntu-latest
13+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
1414
ocaml-compiler:
1515
- 4.14.x
1616

‎.github/workflows/locked.yml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ jobs:
1717
fail-fast: false
1818
matrix:
1919
os:
20-
- ubuntu-latest
20+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
2121
- macos-13
2222
ocaml-compiler:
2323
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
@@ -42,7 +42,7 @@ jobs:
4242
ocaml-compiler: ${{ matrix.ocaml-compiler }}
4343

4444
- name: Install graph-easy # TODO: remove if depext --with-test works
45-
if: ${{ matrix.os == 'ubuntu-latest' }}
45+
if: ${{ matrix.os == 'ubuntu-22.04' }}
4646
run: sudo apt install -y libgraph-easy-perl
4747

4848
- name: Install dependencies
@@ -70,7 +70,7 @@ jobs:
7070
fail-fast: false
7171
matrix:
7272
os:
73-
- ubuntu-latest
73+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
7474
ocaml-compiler:
7575
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
7676
# don't add any other because they won't be used
@@ -91,7 +91,7 @@ jobs:
9191
ocaml-compiler: ${{ matrix.ocaml-compiler }}
9292

9393
- name: Install graph-easy # TODO: remove if depext --with-test works
94-
if: ${{ matrix.os == 'ubuntu-latest' }}
94+
if: ${{ matrix.os == 'ubuntu-22.04' }}
9595
run: sudo apt install -y libgraph-easy-perl
9696

9797
- name: Install spin
@@ -112,7 +112,7 @@ jobs:
112112
fail-fast: false
113113
matrix:
114114
os:
115-
- ubuntu-latest
115+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
116116
ocaml-compiler:
117117
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
118118
# don't add any other because they won't be used

‎.github/workflows/unlocked.yml‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ jobs:
1515
fail-fast: false
1616
matrix:
1717
os:
18-
- ubuntu-latest
18+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
1919
- macos-13
2020
ocaml-compiler:
2121
- 5.2.x
@@ -30,7 +30,7 @@ jobs:
3030
- false
3131

3232
include:
33-
- os: ubuntu-latest
33+
- os: ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
3434
ocaml-compiler: 4.14.x
3535
z3: true
3636
- os: macos-latest
@@ -52,7 +52,7 @@ jobs:
5252
ocaml-compiler: ${{ matrix.ocaml-compiler }}
5353

5454
- name: Install graph-easy # TODO: remove if depext --with-test works
55-
if: ${{ matrix.os == 'ubuntu-latest' }}
55+
if: ${{ matrix.os == 'ubuntu-22.04' }}
5656
run: sudo apt install -y libgraph-easy-perl
5757

5858
- name: Install dependencies
@@ -90,7 +90,7 @@ jobs:
9090
fail-fast: false
9191
matrix:
9292
os:
93-
- ubuntu-latest
93+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
9494
- macos-13
9595
ocaml-compiler:
9696
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
@@ -112,7 +112,7 @@ jobs:
112112
ocaml-compiler: ${{ matrix.ocaml-compiler }}
113113

114114
- name: Install graph-easy # TODO: remove if depext --with-test works
115-
if: ${{ matrix.os == 'ubuntu-latest' }}
115+
if: ${{ matrix.os == 'ubuntu-22.04' }}
116116
run: sudo apt install -y libgraph-easy-perl
117117

118118
- name: Install dependencies
@@ -187,7 +187,7 @@ jobs:
187187
fail-fast: false
188188
matrix:
189189
os:
190-
- ubuntu-latest
190+
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
191191
- macos-13
192192
ocaml-compiler:
193193
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
@@ -204,7 +204,7 @@ jobs:
204204
ocaml-compiler: ${{ matrix.ocaml-compiler }}
205205

206206
- name: Install graph-easy # TODO: remove if depext --with-test works
207-
if: ${{ matrix.os == 'ubuntu-latest' }}
207+
if: ${{ matrix.os == 'ubuntu-22.04' }}
208208
run: sudo apt install -y libgraph-easy-perl
209209

210210
- name: Install Goblint with test

‎conf/svcomp-validate.json‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
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+
"abortUnless",
35+
"unassume"
36+
],
37+
"path_sens": [
38+
"mutex",
39+
"malloc_null",
40+
"uninit",
41+
"expsplit",
42+
"activeSetjmp",
43+
"memLeak",
44+
"threadflag"
45+
],
46+
"context": {
47+
"widen": false
48+
},
49+
"base": {
50+
"arrays": {
51+
"domain": "partitioned"
52+
}
53+
},
54+
"race": {
55+
"free": false,
56+
"call": false
57+
},
58+
"autotune": {
59+
"enabled": true,
60+
"activated": [
61+
"singleThreaded",
62+
"mallocWrappers",
63+
"noRecursiveIntervals",
64+
"enums",
65+
"congruence",
66+
"octagon",
67+
"wideningThresholds",
68+
"loopUnrollHeuristic",
69+
"memsafetySpecification",
70+
"termination",
71+
"tmpSpecialAnalysis"
72+
]
73+
},
74+
"widen": {
75+
"tokens": true
76+
}
77+
},
78+
"exp": {
79+
"region-offsets": true
80+
},
81+
"solver": "td3",
82+
"sem": {
83+
"unknown_function": {
84+
"spawn": false
85+
},
86+
"int": {
87+
"signed_overflow": "assume_none"
88+
},
89+
"null-pointer": {
90+
"dereference": "assume_none"
91+
}
92+
},
93+
"witness": {
94+
"graphml": {
95+
"enabled": false
96+
},
97+
"yaml": {
98+
"enabled": false,
99+
"strict": true,
100+
"format-version": "2.0",
101+
"entry-types": [
102+
"location_invariant",
103+
"loop_invariant",
104+
"invariant_set",
105+
"violation_sequence"
106+
],
107+
"invariant-types": [
108+
"location_invariant",
109+
"loop_invariant"
110+
]
111+
},
112+
"invariant": {
113+
"loop-head": true,
114+
"after-lock": true,
115+
"other": true
116+
}
117+
},
118+
"pre": {
119+
"enabled": false
120+
}
121+
}

‎conf/svcomp.json‎

Lines changed: 1 addition & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -45,27 +45,6 @@
4545
"context": {
4646
"widen": false
4747
},
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-
},
6948
"base": {
7049
"arrays": {
7150
"domain": "partitioned"
@@ -128,17 +107,7 @@
128107
"after-lock": false,
129108
"other": false,
130109
"accessed": false,
131-
"exact": true,
132-
"exclude-vars": [
133-
"tmp\\(___[0-9]+\\)?",
134-
"cond",
135-
"RETURN",
136-
"__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
137-
".*____CPAchecker_TMP_[0-9]+",
138-
"__VERIFIER_assert__cond",
139-
"__ksymtab_.*",
140-
"\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
141-
]
110+
"exact": true
142111
}
143112
},
144113
"pre": {

‎docs/developer-guide/testing.md‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,19 @@ Other useful constructs are the following:
6969
| `__goblint_check(1); // reachable` | Checks that the line is reachable according <br> to Goblint results (soundness). |
7070
| `__goblint_check(0); // NOWARN (unreachable)` | Checks that the line is unreachable (precision). |
7171

72+
#### Meta
73+
Comments at the end of lines can also indicate metaproperties:
74+
75+
| Annotation | Expected result/comment |
76+
| ---------- | ----- |
77+
| `NOCRASH` | No analyzer crash |
78+
| `FIXPOINT` | No fixpoint error |
79+
| `NOTIMEOUT` | Analyer terminates |
80+
| `CRAM` | Automatic checks are only in corresponding Cram test |
81+
82+
These comments only document the intention of the test (if there are no other checks in the test).
83+
Analyzer crash, fixpoint error and non-termination are checked even when there are other checks.
84+
7285
## Cram Tests
7386
[Cram-style tests](https://dune.readthedocs.io/en/stable/tests.html#cram-tests) are also used to verify that existing functionality hasn't been broken.
7487
They check the complete standard output of running the Goblint binary with specified command-line arguments.

‎dune-project‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
4545
(ppx_deriving (>= 6.0.2))
4646
(ppx_deriving_hash (>= 0.1.2))
4747
(ppx_deriving_yojson (>= 3.7.0))
48+
(ppx_blob (>= 0.8.0))
4849
(ppxlib (>= 0.30.0)) ; ppx_easy_deriving
4950
(ounit2 :with-test)
5051
(qcheck-ounit :with-test)

‎goblint.opam‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ depends: [
4545
"ppx_deriving" {>= "6.0.2"}
4646
"ppx_deriving_hash" {>= "0.1.2"}
4747
"ppx_deriving_yojson" {>= "3.7.0"}
48+
"ppx_blob" {>= "0.8.0"}
4849
"ppxlib" {>= "0.30.0"}
4950
"ounit2" {with-test}
5051
"qcheck-ounit" {with-test}
@@ -96,7 +97,11 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
9697
# also remember to generate/adjust goblint.opam.locked!
9798
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
9899
pin-depends: [
99-
[ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
100+
[ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ]
101+
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
102+
[ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
103+
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
104+
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
100105
]
101106
depexts: [
102107
["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

0 commit comments

Comments
 (0)