Julian Erhard

If there is a `current_node` set, and `annotation.int.enabled` is enabled, the values constructed by the `IntDomTuple` will have the precision of the function the node is part of. That also...

@sim642 I had a look at trying to fix this with the approach of passing a `precicision` to all `IntDomTuple` functions that create new values (`of_int`, `of_excl_list`, `of_interval`, `top_of` ...),...

It seems to me, that it would be more suited to ensure that the `current_node` is set correctly on a `join` than to pass the `precision` around in so many...

@michael-schwarz suggested adding a short circuiting physical equality check to the `HoarePO.equal`, i.e. ``` let equal x y = x == y || leq x y && leq y x...

The unsoundness of comparing addresses with a struct field and an index as offsets is also exhibited for non-zero offsets: https://github.com/goblint/analyzer/blob/712c6cef810aa3c6635a677bc9eef7dd8e7cc599/tests/regression/02-base/93-ad-struct-offset.c#L9-L27 The alignment of fields within objects is implementation defined,...

I ran Goblint with short-circuit evalution for the `SensitiveDomain.Projective.equal` (branch `master_hoaredomain-new_short_circuit_equal`) and without it (branch `master_hoaredomain-new`) on sqlite. For the diff, see [here](https://github.com/goblint/analyzer/compare/master_hoaredomain-new...master_hoaredomain-new_short_circuit_equal). Goblint command line ``` time ./goblint_master_hoaredomain-new_short_circuit_equal ../../benchmarks/sqlite-amalgamation-3370200/sqlite3.c...

>I'm not sure anymore, but maybe Environment.t or Var.t is missing serialization/deserialization in Apron Yes. What I did in #433 was to write marshal/unmarshal functions in OCaml that converts the...

>If the new fields are added to the end of the struct, then it should still be compatible as long as those functions aren't called (any non-default var implementations would...

@michael-schwarz and I discussed this before – for the server mode, the marshalling is not inherently necessary, so the Apron analysis should work in the incremental server mode.

>Is the plan here to then also add intervals [a,b] that are not normal in the sense that a