analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
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...
Since #1021 we now have the concept of wrappers around thread creation. We should look at the SV-COMP benchmarks and determine which wrappers appear there often to set a useful...
For the sv-comp benchmarks with annotations we contributed to #855, producing witnesses drastically increased runtime of a context-insensitive analysis from 2mins to 16mins, meaning we could not solve these, even...
For the analysis of large programs, the autotuner should set the analysis to be context-insensitive, following the heuristic that context-insensitive analyses tend to terminate more quickly.
This PR is a first quick draft of adding support for the detection of CWE-562. It's still WIP and since it's probably not directly relevant for SV-COMP, I'd say it...
#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...
This is meant to address two issues we became aware of about escaped variables and the region analysis. - [x] Simply handling pthread arguments and treating escaped variables as globals,...
Goblint is currently not sound in some cases when dealing with offsets taken on casted pointers. ### 1. Comparison of casted pointers with offsets On the current `master`, `Goblint` claims...
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++;...
The following snippet, extracted from concrat/Mirai-Source-Code, crashes Goblint: ```c // PARAM: --enable ana.float.interval // Extracted from concrat/Mirai-Source-Code. extern int ( /* missing proto */ ceil)() ; int main() { int...