You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: .github/workflows/docker.yml
+2-2
Original file line number
Diff line number
Diff line change
@@ -59,7 +59,7 @@ jobs:
59
59
60
60
- name: Build Docker image
61
61
id: build
62
-
uses: docker/build-push-action@v5
62
+
uses: docker/build-push-action@v6
63
63
with:
64
64
context: .
65
65
load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
72
72
run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
@@ -74,10 +74,10 @@ For more information on the signature of the individual transfer functions, plea
74
74
## Extending the domain
75
75
76
76
You could now enrich the lattice to also have a representation for non-negative (i.e., zero or positive) values.
77
-
Then the join of `Zero` and `Pos` would be "non-negative" instead of `Top`, allowing you to prove that such join is greated than `Neg`.
77
+
Then the join of `Zero` and `Pos` would be "non-negative" instead of `Top`, allowing you to prove that such join is greater than `Neg`.
78
78
For example, have a look at the following program: `tests/regression/99-tutorials/02-first-extend.c`.
79
79
80
80
_Hint:_
81
81
The easiest way to do this is to use the powerset lattice of `{-, 0, +}`.
82
82
For example, "non-negative" is represented by `{0, +}`, while negative is represented by `{-}`.
83
-
To do this, modify `SL` by using `SetDomain.FiniteSet` (takes a `struct` with a list of finite elements as second parameter) instead of `Lattice.Flat` and reimplementing the two functions using `singleton` and `for_all`.
83
+
To do this, modify `SL` by using `SetDomain.FiniteSet` (which needs a finite list of elements to be added to `Signs`) instead of `Lattice.Flat` and reimplementing the two functions using `singleton` and `for_all`.
Copy file name to clipboardExpand all lines: docs/user-guide/assumptions.md
+19
Original file line number
Diff line number
Diff line change
@@ -17,3 +17,22 @@ _NB! This list is likely incomplete._
17
17
18
18
See [PR #1414](https://github.com/goblint/analyzer/pull/1414).
19
19
20
+
2. Pointer arithmetic does not overflow.
21
+
22
+
[C11's N1570][n1570] at 6.5.6.8 states that
23
+
24
+
> When an expression that has integer type is added to or subtracted from a pointer, the result has the type of the pointer operand.
25
+
> [...]
26
+
> the evaluation shall not produce an overflow; otherwise, the behavior is undefined.
27
+
28
+
after a long list of defined behaviors.
29
+
30
+
Goblint does not report overflow and out-of-bounds pointer arithmetic (when the pointer _is not dereferenced_).
31
+
This affects the overflow analysis (SV-COMP no-overflow property) in the `base` analysis.
32
+
33
+
This _does not_ affect the `memOutOfBounds` analysis (SV-COMP valid-memsafety property), which is for undefined behavior from _dereferencing_ such out-of-bounds pointers.
34
+
35
+
See [PR #1511](https://github.com/goblint/analyzer/pull/1511).
(authors "Simmo Saan""Michael Schwarz""Julian Erhard""Sarah Tilscher""Ralf Vogler""Kalmer Apinis""Vesal Vojdani"); same authors as in .zenodo.json and CITATION.cff
18
+
(authors "Simmo Saan""Michael Schwarz""Julian Erhard""Sarah Tilscher""Karoliine Holter""Ralf Vogler""Kalmer Apinis""Vesal Vojdani"); same authors as in .zenodo.json and CITATION.cff
Goblint is a sound static analysis framework for C programs using abstract interpretation.
27
+
It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
28
+
Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
29
+
")
30
+
(tags (
31
+
"program analysis"
32
+
"program verification"
33
+
"static analysis"
34
+
"abstract interpretation"
35
+
"C"
36
+
"data race analysis"
37
+
"concurrency"))
25
38
(depends
26
39
(ocaml (>= 4.14))
27
40
(goblint-cil (>= 2.0.3)); TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
28
41
(batteries (>= 3.5.1))
29
42
(zarith (>= 1.10))
30
43
(yojson (>= 2.0.0))
31
44
(qcheck-core (>= 0.19))
32
-
ppx_deriving
45
+
(ppx_deriving(>= 6.0.2))
33
46
(ppx_deriving_hash (>= 0.1.2))
34
47
(ppx_deriving_yojson (>= 3.7.0))
35
48
(ounit2 :with-test)
@@ -54,7 +67,7 @@
54
67
conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS
0 commit comments