Simmo Saan

Results 506 comments of Simmo Saan

Since the release on opam-repository, all our nightly unlocked CI builds fail spectacularly, so I'll just merge these fixes before #1522. A 1 minute sv-benchmarks run didn't reveal any new...

The test uses `(lang dune 2.8)` which might be why it works there, but some newer dune lang might change the behavior.

That's true and that can even be true without things like Apron. If the C stack happens to exactly overflow during some OCaml runtime implementation (in C), then that could...

#1522 doesn't seem to have helped with this, sadly. https://github.com/avsm/ocaml-yaml/pull/75 fixed a segfault in YAML with large values, but that doesn't seem to have been the case here.

I just noticed something in my latest ghost witness generation runs (https://goblint.cs.ut.ee/results/188-concurrency-witness-simpl/table-generator.table.html#/table): there are no segfaults in the non-relational-only runs and there are segfaults in the relational runs. So maybe...

After a day of debugging, I think I found camlidl of all things to be the cause: https://github.com/xavierleroy/camlidl/pull/29. Apron uses camlidl to generate the bindings.

I found some hand-written instances in Apron itself as well: https://github.com/antoinemine/apron/pull/112.

I now did a sv-benchmarks run with the camlidl and Apron fixes on top of #1522: all segfaults now disappeared.

Since this has been fixed in upstream repositories, but not yet released to opam, I've added opam pins for them for now. There's nothing more for us to do about...

> Ideally, one would like to be able to dynamically switch between Apron and Elina. Is this planned? I think the cleanest way would be not to even have them...