Simmo Saan
Simmo Saan
> Above, I wanted to show a smaller fraction of the compile code rather the whole thing that was overwhelming I see. _Soundly_ analyzing incomplete programs is difficult though. For...
> After increasing the VM memory it finished the analysis in 2460 seconds. Just wondering: is this with the default configuration on the entire project or did you need to...
The "conf." stands for "confidence", but it can practically be ignored. It's more of a historical thing that roughly tried to convey, how directly (or indirectly through pointers) the access...
In terms of SV-COMP, I think the act of returning such address wouldn't be considered a violation, but if it is then dereferenced, it would be an invalid dereference.
> * Verify if these are really all changes needed for `mutex-meet-atomic` (It seems weird that no handling of these cases is necessary in `get_mutex_global_g_with_mutex_inits_atomic` CC: @sim642) That doesn't restrict...
`mutex:[__VERIFIER_atomic]` also starts out with `bottom (env: [||])`, so that's not the difference I suspect. Rather, the difference comes from this check: https://github.com/goblint/analyzer/blob/896f236c98ba829aee25e5f02cb08d4bb2bba9b1/src/analyses/apron/relationPriv.apron.ml#L500-L504 `get_mutex_global_g_with_mutex_inits_atomic` doesn't have such condition and always...
No need to overcomplicate the tagging: git is distributed after all. The tag can be created and pushed to the branch in the fork. If this PR is merged, the...
Whether the validation time is excessive depends mostly on how long the analysis takes when all the same invariants are integrated as assertions and done during the analysis. Assert-instrumentation probably...
I suspect the `SetDomain.Unsupported` code is some legacy thing that never even happens now. `AddressSet.top` isn't a lifted `Top` but a normal (foldable-over) set with `UnknownPtr` in it. And `update_one`...
The expected outcome is that for `int` it is `[-31,31]`, not `[-31,32]`, and for `short` it is `[-15,15]`, not `[-15,16]`, because those are the normal bit ranges for those types....