analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
For the program ~~~C extern void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); void reach_error() { __assert_fail("0",...
Base analysis is full of code like ```ocaml set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [...] ``` where `Analyses.ask_of_ctx ctx`, `gs` and `st` are directly taken from `ctx` itself. There's no...
When running the following modifications of test `01-oob-heap-simple.c`: ```c // PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval #include int main(int argc, char const *argv[]) { char *ptr = malloc(5 * sizeof(char));...
If all analyses are context insensitive, the sv-comp testcase `goblint-regression/06-symbeq_04-funloop_hard1.i` fails with the `svcomp24.json` configuration. It seems that some analyses produce unsound results if they are analyzed context-insensitively. To set...
This is the same scenario as in issue #1298. All analyses are set context-insensitively, and the sv-comp test `goblint-regression/06-symbeq_04-funloop_hard1.i` is analyzed with the `svcomp24` configuration. As stated in #1298 the...
We can reject violation witnesses for programs that we can prove correct, assuming we are sound. This probably won't make us very good in the validation track though. We could...
The move from separate `location_invariant` and `loop_invariant` entries to one `invariant_set` entry in YAML witnesses had an unintended consequence: all invariants from the set are tagged with the same UUID...
Changes needed for the "**Test Automation for Incremental Analysis - TAIA**" from the [pull request in the bench repository](https://github.com/goblint/bench/pull/58): - Add new goblint check annotation `NOFAIL` which expresses the knowledge...
[CWE-562](https://cwe.mitre.org/data/definitions/562.html) is concerned with the issue of returning an address of a stack variable. Here's a minimal example of a program that has a `CWE-562` weakness: ```c char *cwe562() {...
@jerhard and I discovered an issue where we currently are unsound as we do not correctly account for some modifications via globals: ~~~C #include #include int g; int* global =...