Skip to content

Commit

Permalink
Merge branch 'goblint:master' into relational-substring-domain
Browse files Browse the repository at this point in the history
  • Loading branch information
nathanschmidt authored Sep 8, 2023
2 parents 36e66dd + d97504b commit 4eeb1e4
Show file tree
Hide file tree
Showing 57 changed files with 584 additions and 173 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/coverage.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up OCaml ${{ matrix.ocaml-compiler }}
env:
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/docker.yml
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
Expand Down
5 changes: 4 additions & 1 deletion .github/workflows/docs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,10 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Check for undocumented modules
run: python scripts/goblint-lib-modules.py

- name: Set up OCaml ${{ matrix.ocaml-compiler }}
env:
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/indentation.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4
with:
fetch-depth: 0

Expand Down
6 changes: 3 additions & 3 deletions .github/workflows/locked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up OCaml ${{ matrix.ocaml-compiler }}
env:
Expand Down Expand Up @@ -101,7 +101,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up OCaml ${{ matrix.ocaml-compiler }}
env:
Expand Down Expand Up @@ -141,7 +141,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up OCaml ${{ matrix.ocaml-compiler }}
env:
Expand Down
4 changes: 2 additions & 2 deletions .github/workflows/metadata.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Validate CITATION.cff
uses: docker://citationcff/cffconvert:latest
Expand All @@ -36,7 +36,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up Node.js ${{ matrix.node-version }}
uses: actions/setup-node@v3
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/options.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up Node.js ${{ matrix.node-version }}
uses: actions/setup-node@v3
Expand Down
4 changes: 2 additions & 2 deletions .github/workflows/semgrep.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,10 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Run semgrep
run: semgrep scan --sarif --output=semgrep.sarif
run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif

- name: Upload SARIF file to GitHub Advanced Security Dashboard
uses: github/codeql-action/upload-sarif@v2
Expand Down
8 changes: 4 additions & 4 deletions .github/workflows/unlocked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: ocaml/setup-ocaml@v2
Expand Down Expand Up @@ -131,7 +131,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: ocaml/setup-ocaml@v2
Expand Down Expand Up @@ -208,7 +208,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
Expand Down Expand Up @@ -246,7 +246,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: ocaml/setup-ocaml@v2
Expand Down
1 change: 1 addition & 0 deletions .semgrep/tracing.yml
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ rules:
- pattern: Messages.traceu
- pattern: Messages.traceli
- pattern-not-inside: if Messages.tracing then ...
- pattern-not-inside: if Messages.tracing && ... then ...
message: trace functions should only be called if tracing is enabled at compile time
languages: [ocaml]
severity: WARNING
8 changes: 0 additions & 8 deletions conf/bench-yaml-validate.json
Original file line number Diff line number Diff line change
Expand Up @@ -52,14 +52,6 @@
"tokens": true
}
},
"witness": {
"enabled": false,
"invariant": {
"loop-head": true,
"after-lock": true,
"other": false
}
},
"sem": {
"unknown_function": {
"invalidate": {
Expand Down
14 changes: 0 additions & 14 deletions conf/bench-yaml.json
Original file line number Diff line number Diff line change
Expand Up @@ -48,20 +48,6 @@
]
}
},
"witness": {
"enabled": false,
"yaml": {
"enabled": true
},
"invariant": {
"exact": false,
"exclude-vars": [
"tmp\\(___[0-9]+\\)?",
"cond",
"RETURN"
]
}
},
"sem": {
"unknown_function": {
"invalidate": {
Expand Down
13 changes: 5 additions & 8 deletions conf/svcomp-yaml-validate.json
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,10 @@
"float": {
"interval": true
},
"apron": {
"domain": "polyhedra",
"strengthening": true
},
"activated": [
"base",
"threadid",
Expand All @@ -31,6 +35,7 @@
"region",
"thread",
"threadJoins",
"apron",
"unassume"
],
"context": {
Expand Down Expand Up @@ -74,14 +79,6 @@
"exp": {
"region-offsets": true
},
"witness": {
"enabled": false,
"invariant": {
"loop-head": true,
"after-lock": false,
"other": false
}
},
"solver": "td3",
"sem": {
"unknown_function": {
Expand Down
10 changes: 9 additions & 1 deletion conf/svcomp-yaml.json
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,10 @@
"float": {
"interval": true
},
"apron": {
"domain": "polyhedra",
"strengthening": true
},
"activated": [
"base",
"threadid",
Expand All @@ -30,7 +34,8 @@
"symb_locks",
"region",
"thread",
"threadJoins"
"threadJoins",
"apron"
],
"context": {
"widen": false
Expand Down Expand Up @@ -76,6 +81,9 @@
"enabled": true
},
"invariant": {
"loop-head": true,
"other": false,
"accessed": false,
"exact": false,
"exclude-vars": [
"tmp\\(___[0-9]+\\)?",
Expand Down
59 changes: 59 additions & 0 deletions scripts/goblint-lib-modules.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
#!/usr/bin/python3

from pathlib import Path
import re
import sys

src_root_path = Path("./src")

goblint_lib_path = src_root_path / "goblint_lib.ml"
goblint_lib_modules = set()

with goblint_lib_path.open() as goblint_lib_file:
for line in goblint_lib_file:
line = line.strip()
m = re.match(r"module (.*) = .*", line)
if m is not None:
module_name = m.group(1)
goblint_lib_modules.add(module_name)

src_vendor_path = src_root_path / "vendor"
exclude_module_names = set([
"Goblint_lib", # itself

# executables
"Goblint",
"MessagesCompare",
"PrivPrecCompare",
"ApronPrecCompare",
"Mainspec",

# libraries
"Goblint_timing",
"Goblint_backtrace",
"Goblint_sites",
"Goblint_build_info",

"MessageCategory", # included in Messages
"PreValueDomain", # included in ValueDomain
"SpecCore", # spec stuff
"SpecUtil", # spec stuff
])

src_modules = set()

for ml_path in src_root_path.glob("**/*.ml"):
if str(ml_path).startswith(str(src_vendor_path)):
continue

module_name = ml_path.with_suffix("").with_suffix("").name
module_name = module_name[0].upper() + module_name[1:]
if module_name.endswith("0") or module_name.endswith("_intf") or module_name in exclude_module_names:
continue

src_modules.add(module_name)

missing_modules = src_modules - goblint_lib_modules
if len(missing_modules) > 0:
print(f"Modules missing from {goblint_lib_path}: {missing_modules}")
sys.exit(1)
Loading

0 comments on commit 4eeb1e4

Please sign in to comment.