Simmo Saan
Simmo Saan
> but do not modify the underlying hash-table in that the computed hashes should stay the same regardless of hash-consing or not. They create a new hashtable and add all...
The deadlock analysis uses a set of may lock _events_, consisting of: 1. the mutex, 2. the node where it was locked, 3. the `MCPAccess` data at that point. In...
It seems like a slight variation of `thread` analysis could work for the multithreaded case as well. And it would avoid having to hammer yet another feature into `base` analysis...
This assumes we first abstract our apron analysis away from Apron. This is partially supposed to be done in #592, but AFAIK that still keeps `Apron.Environment` and `Apron.Var` in the...
I looked at Elina's OCaml package: https://ocaml.org/p/elina/1.3.2/doc/Elina_oct/index.html. Actually you're right about that: it depends on Apron and uses Apron types for most things. All it really does it provide two...
This is interesting because the `destabilize_with_side` used for restarting is just based on the old `destabilize`, of course neither is tail recursive. It's just TD3's `solve` which is tail recursive....
The fact that an SV-COMP program redefines a standard function is arguably not allowed and I've proposed to have it changed, including this benchmark: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1358. Although I think we didn't...
The sv-benchmarks MR has been merged and this is no longer unsound in the preruns.
There's quite an extensive description of all our Hoare-(like) domains in #101, so maybe I'll have to think about this Hoare and partitioning stuff again. > The implementation of `HoareDomain.equal`...
And another thing to look at (depending on which of the two is the culprit): how many elements do the Hoare sets in question actually have? It could be that...