Simmo Saan

The script is supposed to always run under bash though: https://github.com/goblint/analyzer/blob/2f5afc2c23fa12bbc1572f3fef43b5fa8cc0fa5e/make.sh#L1 Is that not happening for you? I guess Manjaro/Arch doesn't install the `gcc-12` symlink then, so this hacky version...

In SV-COMP 2022 we timed out on this task after 960s, by the way.

I believe this benchmark has UB. `usb_altnum_to_altsetting` `malloc`s some memory into `alt` and then reads from it without initializing anything. At `ep = & (alt->endpoint + (unsigned long )j)->desc;` due...

Interesting, I wasn't aware of that output, although it's somewhat different, because there the idea is to regularly print the same statistics. For benchmarking results overview and comparison it's just...

> * Ghost variable `len$array$` that is set to `len` on malloc and then automatically tracks the length How do you imagine this working? That there's a pre-transformation of the...

I see @michael-schwarz has just started documenting _something_ for the SAS21 artifact (https://github.com/goblint/analyzer/tree/sas21_artifact_description), but we should probably have a broader strategy for this.

Of course there's no point in writing massive documentation just for the sake of it when it's too much to keep up to date, but the tutorial-like use case is...

I added these ideas into the issue itself, to have a nice TODO list at the top. If any others come about, feel free to edit the issue to extend...

I decided to set up Read the Docs now because it's actually quite unintrusive: all the documentation is based on the contents of the `./docs` directory and can also be...

I think we already handle the usual suspects as non-returning: https://github.com/goblint/analyzer/blob/e81b1a147f420983583e680a57d8a6d8b071ca68/src/analyses/base.ml#L2188-L2205 Of course I guess a modern standard library header would also have them with `_Noreturn` (or equivalent). Actually it...