-
Notifications
You must be signed in to change notification settings - Fork 76
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' into yaml-witness-ghost
- Loading branch information
Showing
59 changed files
with
678 additions
and
134 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,123 @@ | ||
| { | ||
| "ana": { | ||
| "sv-comp": { | ||
| "enabled": true, | ||
| "functions": true | ||
| }, | ||
| "int": { | ||
| "def_exc": true, | ||
| "enums": false, | ||
| "interval": true | ||
| }, | ||
| "float": { | ||
| "interval": true, | ||
| "evaluate_math_functions": 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 | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,118 @@ | ||
| { | ||
| "ana": { | ||
| "sv-comp": { | ||
| "enabled": true, | ||
| "functions": true | ||
| }, | ||
| "int": { | ||
| "def_exc": true, | ||
| "enums": false, | ||
| "interval": true | ||
| }, | ||
| "float": { | ||
| "interval": true, | ||
| "evaluate_math_functions": true | ||
| }, | ||
| "activated": [ | ||
| "base", | ||
| "threadid", | ||
| "threadflag", | ||
| "threadreturn", | ||
| "mallocWrapper", | ||
| "mutexEvents", | ||
| "mutex", | ||
| "access", | ||
| "race", | ||
| "escape", | ||
| "expRelation", | ||
| "mhp", | ||
| "assert", | ||
| "var_eq", | ||
| "symb_locks", | ||
| "region", | ||
| "thread", | ||
| "threadJoins", | ||
| "abortUnless" | ||
| ], | ||
| "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" | ||
| ] | ||
| } | ||
| }, | ||
| "exp": { | ||
| "region-offsets": true | ||
| }, | ||
| "solver": "td3", | ||
| "sem": { | ||
| "unknown_function": { | ||
| "spawn": false | ||
| }, | ||
| "int": { | ||
| "signed_overflow": "assume_none" | ||
| }, | ||
| "null-pointer": { | ||
| "dereference": "assume_none" | ||
| } | ||
| }, | ||
| "witness": { | ||
| "graphml": { | ||
| "enabled": true, | ||
| "id": "enumerate", | ||
| "unknown": false | ||
| }, | ||
| "yaml": { | ||
| "enabled": true, | ||
| "format-version": "2.0", | ||
| "entry-types": [ | ||
| "invariant_set" | ||
| ], | ||
| "invariant-types": [ | ||
| "loop_invariant" | ||
| ] | ||
| }, | ||
| "invariant": { | ||
| "loop-head": true, | ||
| "after-lock": false, | ||
| "other": false, | ||
| "accessed": false, | ||
| "exact": true | ||
| } | ||
| }, | ||
| "pre": { | ||
| "enabled": false | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -16,7 +16,7 @@ | |
| (homepage "https://goblint.in.tum.de") | ||
| (documentation "https://goblint.readthedocs.io/en/latest/") | ||
| (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 | ||
| (maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>" "Karoliine Holter") | ||
| (maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>" "Karoliine Holter <[email protected]>") | ||
| (license MIT) | ||
|
|
||
| (package | ||
|
|
@@ -37,7 +37,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e | |
| "concurrency")) | ||
| (depends | ||
| (ocaml (>= 4.14)) | ||
| (goblint-cil (>= 2.0.4)) ; 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. | ||
| (goblint-cil (>= 2.0.5)) ; 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. | ||
| (batteries (>= 3.5.1)) | ||
| (zarith (>= 1.10)) | ||
| (yojson (>= 2.0.0)) | ||
|
|
||
Oops, something went wrong.