Simmo Saan

This is a quick proof-of-concept for an idea I had a while ago: unassume for variable protection in mutex analysis. It is the first example of a non–value-domain unassume operator....

Total LLoC depends on analysis

4

While writing up my thesis I found that the total LLoC we report for some benchmarks differs between three papers: | Benchmark | [traces paper](https://link.springer.com/chapter/10.1007/978-3-030-88806-0_18) | [more-traces paper](https://link.springer.com/chapter/10.1007/978-3-031-30044-8_2) | [unassume...

Audit for domain-unsafe global code

1

Initial list from #1708 reviews, but could be extended over time: - [ ] Top-level `lazy` values: - [ ] `Offset.Index.Exp.all` - [ ] `Cilfacade.any_index_exp` - [ ] `LibraryFunctions.intmax_t` -...

> I just realized we have a bit of an inconsistency with how our relation and Apron stuff are split. This analysis is also applied for our OCaml-implemented relational domains,...

`longjmp` in abstract call graph/ARG

5

The termination analysis uses an abstract call graph to detect cycles from recursion. As far as I know, this graph does not contain edges corresponding to `longjmp` flows. Instead, the...

Add explicit W set to base protection privatization

3

Regarding https://github.com/goblint/analyzer/pull/1636#discussion_r1963055883. Surprisingly, there was even a TODO about it: https://github.com/goblint/analyzer/blob/a9354564fbb6b3d86879a4949f9d93c04399584c/src/analyses/basePriv.ml#L940-L943