Simmo Saan
Simmo Saan
This PR conflicts with #845 due to the changes in stubs structure. ### TODO - [x] Add autotune conf
In #859 one of the autotune unsoundness cases was caused by autotune deactivating the threadflag analysis. A minimized TODO test is added here: https://github.com/goblint/analyzer/pull/859/commits/505b66949e488060daf82413a399b328d05b4ebc. The problem is, when threadflag is...
Closes #814. ### TODO - [ ] Before merging this into master, merge master into this and make same changes in all the tests added on master meanwhile.
Since we know where dead code is and can output C programs via CIL, we could have a transformation that removes all the dead code from the program. It wouldn't...
Now that we have cram from #787, it's a good time to use it to automate previously manual tests. ### Changes 1. Add tests for YAML witness generation. The `yamlWitnessStrip`...
While trying to squeeze maximum performance out of #796, I at some point completely removed this layer for some speedup I guess, but not to remove features, this is an...
In some special cases it's desirable to spawn threads as non-unique right off the bat: 1. Unknown functions which spawn create unique threads: https://github.com/goblint/analyzer/pull/837#discussion_r984570708. This is unsound and we should...
In my own run of Goblint on SV-COMP SoftwareSystems category, Goblint crashed with ``` exception Failure("Type mismatch!") ``` https://github.com/goblint/analyzer/blob/3164939e27b7908839fe083f036ca165eb54d7ea/src/cdomains/lval.ml#L508-L514 from region analysis domain (which uses `PartitionDomain` and `collapse` functions) on...
As revealed in #388, it would be very good to have an unknown thread ID, just like the unknown address in address sets. This would allow keeping known thread IDs...
This issue is to document possible improvements and fixes to the regression2sv-benchmarks script. Not intended to be done for SV-COMP 2022 any more. - [ ] Support multi-property benchmarks. Technically...