analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
Otherwise, `project` will only create tops in the new domain which are never refined. We should either check that we are not using annotations for different int precisions in different...
Queries like `WarnGlobal` and `InvariantGlobal` are only used globally in dummy `ctx`. Moreover, they have `Obj.t` arguments which are unsafe. Every analysis lifter which adds its own global unknowns must...
Turns out when the octagon autotuner says `Enabled octagon domain for: ...`, it _implicitly_ means "disabling octagon analysis for all other variables, _even if explicitly enabled by the user". This...
During #1412 we encountered several legacy problems in the current state of relational analysis, in `relationDomain.apron.ml` and `sharedFunctions.apron.ml` to be taken care of in some PR: - [x] `relationDomain.apron.ml` module...
As brought up in GobCon, we might want to rename `ctx` because it's not a context in the analysis sense. ### Candidates 1. `man` – manager.
In #975 some code was switched from eagerly-constructed lists to the standard `Seq.t`. However, there's still many places where `BatEnum`/`Enum` is used, which offers similar lazy-sequence functionality. We could try...
#1073 introduced multiplicity counters for recursive mutexes in must-locksets. As hinted in https://github.com/goblint/analyzer/pull/1073#discussion_r1217962573, this is simply a multiset domain. However, the implementation keeps a map of multiplicities in addition to...
As #1413 and the associated regressions show, having more precise (and potentially fewer) contexts is not always beneficial when attempting to prove termination of recursive programs (when we have partial...
The C standard says: > If the size of the space requested is zero, the behavior is implementation defined: either a null pointer is returned, or the behavior is as...
As a follow-up of #1414 this documents one further instance where we make assumptions (implementation-defined behavior follows GCC).