Simmo Saan
Simmo Saan
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...
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...
https://github.com/awslabs/one-line-scan/ is some kind of helper tool for running various fuzzers and analyzers. For example, they support CBMC and Infer. Looks like it's supposed to make using those tools easier...
SV-COMP and BenchExec can give the task time limit to the tool. Goblint doesn't use this information and just keeps running after the BenchExec soft time limit until it is...
In addition to Pthread, library function specifications should be added for C11 concurrency functions: https://en.cppreference.com/w/c/thread. These should hopefully be very similar to the Pthread ones and map to the same...
We have a heuristic for outputting witness invariants at loop heads, which more-or-less should match with widening points, but it outputs invariants for all variables, not just those that required...
Currently the autotuner looks for any special function of the `ThreadCreate` kind to determine if multi-threaded analysis is needed or not. As pointed out in https://github.com/goblint/analyzer/pull/1174#discussion_r1331129926, this check is insufficient...
#1093 leaves a bunch of things to clean up after merging for SV-COMP 2024: - [ ] Clarify and document new test annotations: https://github.com/goblint/analyzer/pull/1093#discussion_r1356945296. - [ ] Fix incremental analysis...
Given the following program: ```c // PARAM: --set ana.int.refinement fixpoint --enable ana.int.interval // FIXPOINT #include int g = 0; void main() { int i = 0; while (1) { i++;...