Simmo Saan

Since this is still in need of refactoring/cleanup, it's too late to include for SV-COMP 2024. Four additional tasks out of ~32000 is not worth the risk for a possible...

It's not just about SV-COMP though. It will be _the_ representative version of Goblint for the entire year to come. If something doesn't yet meet our own standards, then it's...

Why is the `TmpSpecialInv` query needed? `TmpSpecial` itself already is a certain inverse (for refining the argument based on the return value), so `TmpSpecialInv` is some kind of inverse of...

This might not be the fault of apron analysis per se because this example involves nested loops, which are known to produce more difficult examples for solvers (by demanding local...

I guess by meaningful analysis you mean Apron should find `loop1 == i` (or offset by one, depending on the node). With `--set sem.int.signed_overflow assume_none` it also does, so the...

Apparently Frama-C realized this at some point as well: ```ocaml (* BIGTODO: this function is not quite a total order, because [is_leq] is only a partial order. Using the hash...

When minimized, this has nothing to do with affine equalities: ```c int main() { int CELLCOUNT; int i; int j; for(i = 1; i = 1; j--) { } }...

Regarding the control flow for `asm goto`, it might be worth looking at what CIL does with computed `goto`s. Because it seems like CIL already converts them to a switch...

This might get a big off-topic, but in what sense is that so ugly. The alternative is having to handle `ComputedGoto` inside Goblint directly, but how would you even construct...

I did an sv-benchmarks run comparing OCaml 4.14 with OCaml 5.0 and the results are concerning. We might have to postpone making OCaml 5.0 the default and simply cherry-pick the...