Simmo Saan
Simmo Saan
During #1394 I implemented ghost witness generation for relational mutex-meet. The benchmarks revealed unsoundness which is also present on master (2fa4f55e682da3ad937e394fe20449eeef4c9634) in: - [x] ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil (#1444) - [x] ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil (#1444)...
In `c/pthread/fib_safe-5.i` from #1356, we produce an unsound invariant. Opening the HTML view to see globals reveals that they somehow have all integer domains enabled: > base:priv:unprotected:cur → def_exc:Unknown int([-31,31]);...
This implements a big portion of #31 using my experimental [ppx_easy_deriving](https://github.com/sim642/ppx_easy_deriving) library. The goal of the library is to provide a simpler [ppx_type_directed_value](https://github.com/janestreet/ppx_type_directed_value/)-like interface with no performance penalty. It is...
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...
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...
For example, given this graph: ```mermaid flowchart LR 1 --> 2 2 --> 1 3 --> 1 3 --> 2 ``` The transitive reduction algorithm yields this one: ```mermaid flowchart...