Skip to content

Commit

Permalink
Merge branch 'master' into yaml-witness-ghost
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Nov 21, 2024
2 parents 8a0240d + 065f990 commit 002fdd3
Show file tree
Hide file tree
Showing 324 changed files with 4,566 additions and 2,564 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/coverage.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
# don't add any other because they won't be used
Expand All @@ -40,7 +40,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

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

- name: Install dependencies
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/docs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ jobs:
strategy:
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
# don't add any other because they won't be used
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/indentation.yml
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ jobs:
strategy:
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- 4.14.x

Expand Down
10 changes: 5 additions & 5 deletions .github/workflows/locked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
- macos-13
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
Expand All @@ -42,7 +42,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

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

- name: Install dependencies
Expand Down Expand Up @@ -70,7 +70,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
# don't add any other because they won't be used
Expand All @@ -91,7 +91,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

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

- name: Install spin
Expand All @@ -112,7 +112,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
# don't add any other because they won't be used
Expand Down
14 changes: 7 additions & 7 deletions .github/workflows/unlocked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
- macos-13
ocaml-compiler:
- 5.2.x
Expand All @@ -30,7 +30,7 @@ jobs:
- false

include:
- os: ubuntu-latest
- os: ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
ocaml-compiler: 4.14.x
z3: true
- os: macos-latest
Expand All @@ -52,7 +52,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

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

- name: Install dependencies
Expand Down Expand Up @@ -90,7 +90,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
- macos-13
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
Expand All @@ -112,7 +112,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

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

- name: Install dependencies
Expand Down Expand Up @@ -187,7 +187,7 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
- macos-13
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
Expand All @@ -204,7 +204,7 @@ jobs:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

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

- name: Install Goblint with test
Expand Down
26 changes: 26 additions & 0 deletions .semgrep/fold.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
rules:
- id: fold-exists
patterns:
- pattern-either:
- pattern: $D.fold ... false
- pattern: $D.fold_left ... false
- pattern: $D.fold_right ... false
- pattern: fold ... false
- pattern: fold_left ... false
- pattern: fold_right ... false
message: consider replacing fold with exists
languages: [ocaml]
severity: WARNING

- id: fold-for_all
patterns:
- pattern-either:
- pattern: $D.fold ... true
- pattern: $D.fold_left ... true
- pattern: $D.fold_right ... true
- pattern: fold ... true
- pattern: fold_left ... true
- pattern: fold_right ... true
message: consider replacing fold with for_all
languages: [ocaml]
severity: WARNING
8 changes: 8 additions & 0 deletions .semgrep/tracing.yml
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,16 @@ rules:
- pattern: Messages.tracec
- pattern: Messages.traceu
- pattern: Messages.traceli
- pattern: M.trace
- pattern: M.tracel
- pattern: M.tracei
- pattern: M.tracec
- pattern: M.traceu
- pattern: M.traceli
- pattern-not-inside: if Messages.tracing then ...
- pattern-not-inside: if Messages.tracing && ... then ...
- pattern-not-inside: if M.tracing then ...
- pattern-not-inside: if M.tracing && ... then ...
message: trace functions should only be called if tracing is enabled at compile time
languages: [ocaml]
severity: WARNING
122 changes: 122 additions & 0 deletions conf/svcomp-validate.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,122 @@
{
"ana": {
"sv-comp": {
"enabled": true,
"functions": true
},
"int": {
"def_exc": true,
"enums": false,
"interval": true
},
"float": {
"interval": true
},
"activated": [
"base",
"threadid",
"threadflag",
"threadreturn",
"mallocWrapper",
"mutexEvents",
"mutex",
"access",
"race",
"escape",
"expRelation",
"mhp",
"assert",
"var_eq",
"symb_locks",
"region",
"thread",
"threadJoins",
"abortUnless",
"unassume"
],
"path_sens": [
"mutex",
"malloc_null",
"uninit",
"expsplit",
"activeSetjmp",
"memLeak",
"threadflag"
],
"context": {
"widen": false
},
"base": {
"arrays": {
"domain": "partitioned"
}
},
"race": {
"free": false,
"call": false
},
"autotune": {
"enabled": true,
"activated": [
"singleThreaded",
"mallocWrappers",
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
"noOverflows",
"termination",
"tmpSpecialAnalysis"
]
},
"widen": {
"tokens": true
}
},
"exp": {
"region-offsets": true
},
"solver": "td3",
"sem": {
"unknown_function": {
"spawn": false
},
"int": {
"signed_overflow": "assume_none"
},
"null-pointer": {
"dereference": "assume_none"
}
},
"witness": {
"graphml": {
"enabled": false
},
"yaml": {
"enabled": false,
"strict": true,
"format-version": "2.0",
"entry-types": [
"location_invariant",
"loop_invariant",
"invariant_set",
"violation_sequence"
],
"invariant-types": [
"location_invariant",
"loop_invariant"
]
},
"invariant": {
"loop-head": true,
"after-lock": true,
"other": true
}
},
"pre": {
"enabled": false
}
}
34 changes: 2 additions & 32 deletions conf/svcomp.json
Original file line number Diff line number Diff line change
Expand Up @@ -45,27 +45,6 @@
"context": {
"widen": false
},
"malloc": {
"wrappers": [
"kmalloc",
"__kmalloc",
"usb_alloc_urb",
"__builtin_alloca",
"kzalloc",

"ldv_malloc",

"kzalloc_node",
"ldv_zalloc",
"kmalloc_array",
"kcalloc",

"ldv_xmalloc",
"ldv_xzalloc",
"ldv_calloc",
"ldv_kzalloc"
]
},
"base": {
"arrays": {
"domain": "partitioned"
Expand All @@ -87,6 +66,7 @@
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
"noOverflows",
"termination",
"tmpSpecialAnalysis"
]
Expand Down Expand Up @@ -128,17 +108,7 @@
"after-lock": false,
"other": false,
"accessed": false,
"exact": true,
"exclude-vars": [
"tmp\\(___[0-9]+\\)?",
"cond",
"RETURN",
"__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
".*____CPAchecker_TMP_[0-9]+",
"__VERIFIER_assert__cond",
"__ksymtab_.*",
"\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
]
"exact": true
}
},
"pre": {
Expand Down
13 changes: 13 additions & 0 deletions docs/developer-guide/testing.md
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,19 @@ Other useful constructs are the following:
| `__goblint_check(1); // reachable` | Checks that the line is reachable according <br> to Goblint results (soundness). |
| `__goblint_check(0); // NOWARN (unreachable)` | Checks that the line is unreachable (precision). |

#### Meta
Comments at the end of lines can also indicate metaproperties:

| Annotation | Expected result/comment |
| ---------- | ----- |
| `NOCRASH` | No analyzer crash |
| `FIXPOINT` | No fixpoint error |
| `NOTIMEOUT` | Analyer terminates |
| `CRAM` | Automatic checks are only in corresponding Cram test |

These comments only document the intention of the test (if there are no other checks in the test).
Analyzer crash, fixpoint error and non-termination are checked even when there are other checks.

## Cram Tests
[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.
They check the complete standard output of running the Goblint binary with specified command-line arguments.
Expand Down
1 change: 1 addition & 0 deletions dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
(ppx_deriving (>= 6.0.2))
(ppx_deriving_hash (>= 0.1.2))
(ppx_deriving_yojson (>= 3.7.0))
(ppx_blob (>= 0.8.0))
(ppxlib (>= 0.30.0)) ; ppx_easy_deriving
(ounit2 :with-test)
(qcheck-ounit :with-test)
Expand Down
Loading

0 comments on commit 002fdd3

Please sign in to comment.