Simmo Saan
Simmo Saan
Closes #1577. These are disabled by default, but can be enabled with `dbg.termination-bounds`. Also cleans up the implementation of `LoopTermination.special` in general (pointless `else ()`, too wide `try` scope, annoying...
Our race analysis can output "proofs" as success messages with `allglobs` enabled. This is useful for inspecting why Goblint believes the program to be correct. We could do something similar...
This was wondered in https://github.com/goblint/analyzer/pull/1485#discussion_r1714983146. We already have special `BotValue` exception that can indicate such thing, but oddly this is not properly lifted by the `LiftBot` functor.
Closes #1572. Also removes `Lattice.Unsupported` by replacing usages with the more specific `BotValue` or `TopValue`. There's also `Lattice.Uncomparable` which seems similar: https://github.com/goblint/analyzer/blob/52817d651f1de47dee935925952ad55e277013db/src/domain/lattice.ml#L14-L15 But #1109 seems to use it with some...
This uses the following lattice property which is true in even non-distributive lattices: $$ a \sqcup (b \sqcap c) \sqsubseteq (a \sqcup b) \sqcap (a \sqcup c) $$ I don't...
The `may_create` function for our history-based thread IDs from the ESOP paper is quite conservative. After thinking about it for a while (in comparison to `is_must_parent`, I noticed many cases...
This is an extension of #1301, which #1512 implemented on a primitive level where the contents of the violation sequence aren't used at all. It should be possible to interpret...
According to https://github.com/ocsigen/js_of_ocaml/issues/1641, our workarounds for using dune build-info and sites with js_of_ocaml are no longer necessary since dune 3.7. They just work now, so things can be simplified. ###...
In the sv-benchmarks run of #1552 with `vojdani` privatization I noticed a particularly odd spurious overflow warning: ``` [Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i:742:3-742:16) ``` The line in question...
In opam-repository CI with Linux arm64, there were failures for the 2.4.0 release like: ``` cpp: error: unrecognized command-line option '-m64' ``` Apparently the `-m64` and `-m32` options are specific...