Michael Schwarz

Spellchecker incorrectly accepts spelling 'decleration'

8

The spellchecker incorrectly accepts `decleration` as a correct word, even though it is an (albeit quite common) misspelling of `declaration`. **Steps to Reproduce** Type `decleration` into an editor window that...

Finalize options, so that they cannot be mutated after the solver started

1

Pulled out from #28 since most of the TODOs there are now done. This would gives us an additional safety guarantee that no options are modified after the solver has...

Re-consider `exp.volatiles_are_top`

3

We currently enable this everywhere, which leads to `volatile` and `extern` variables always having the value `T`. While this is of course safe and makes sense when analyzing e.g. drivers,...

Mutex-Meet-TID Privatization for Base

2

This adds a Mutex-Meet-TID based privatization for Base. TODO: - [x] Tests - [ ] See if more duplication can be avoided between the relational and non-relational analysis During the...

Eager destab, cheap abort

15

This WIP is the Munich idea for aborting. It's still far from polished, just thought I'd open the PR in case someone wants to take a look. TODOs: - [x]...

We should aim to support recursive mutexes more thoroughly: We could e.g. maintain an interval expressing how many times a recursive mutex is locked, or alternatively just maintain if it...

Support for `atexit`, `on_exit` and `pthread_cleanup_*` handlers

2

Those are features we currently do not support yet, but it might be interesting to do so.

Fixpoints not being reached

14

SV-Comp '21 revealed a few example programs where we do not reach the fixpoint: - [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v%2Bcfa-reducer.yml - [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.1.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml - [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v%2Bcfa-reducer.yml - [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.3.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml...

There is no reason we cannot also make use of MHP in the non-relational Mutex-Meet privatization. This should be added such that we can, e.g. profit from MHP information to...

Unsoundness for Two SV-Comp benchmarks

3

- [ ] `ldv-validator-v0.6/linux-stable-af3071a-1-130_7a-drivers--hwmon--s3c-hwmon.ko-entry_point.cil.c` - [ ] `ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--input--touchscreen--usbtouchscreen.ko-entry_point.cil` The first benchmark seem to miss some sort of initialization (setting `s3c_hwmon_driver_group0` to anything other than what `zalloc` yields), which leads to...