Simmo Saan

> On the contrary, it makes the problem even worse since previously `a` and `a[0]` were more-or-less handled equivalently but now they're split into separate buckets. Same with the `a`...

It would also be worth checking if sv-benchmarks even use these. There shouldn't be any `extern`s since the programs are supposed to be closed. There might be `volatile`s though. The...

For an initial migration in Goblint, we could still do that, but maybe with `~width:max_int` so `Pretty` doesn't add line-wrapping newlines. I think the CIL pretty printers for expressions and...

Here's an interesting idea, which might make migration easy, but I don't know if it's possible: Define our own `Pretty` module with `type doc = Format.formatter -> unit` and a...

I immediately remembered this piece of code: https://github.com/goblint/analyzer/blob/0f9f068ee53e181405515191ad8b9ffe66800fc9/src/analyses/base.ml#L1031-L1034 It's reading the global before writing to it. My understanding is that this is necessary for writing into structs/unions/arrays, such that `update_offset`...

I'm not too familiar with the logic there so I don't know, but this thought popped into my mind as well. I guess one must carefully check that they decompose...

If I remember correctly, then indeed octagon implements some serialization/deserialization for its custom OCaml memory blocks, but if that's the case, why do we still get the exception with it?...

> Yes. What I did in #433 was to write marshal/unmarshal functions in OCaml that converts the Environment back and forth to serializable data structures. Right, but there isn't really...

I think with some of the changes from #545, it should be possible to make this work quite easily in server mode, because that PR exposes solver data handling functions...

What's the explanation for closing this without merging?