Simmo Saan comments

Results 487 comments of


                                            Simmo Saan

Use SV-COMP time limit for soft exit

BenchExec should send `SIGTERM` on soft time limit and Goblint does react to it (and doesn't even override the signal handler), but somehow it doesn't work under BenchExec? SV-COMP 2023...

Use SV-COMP time limit for soft exit

I couldn't reproduce this with `runexec` nor under BenchExec. Even with SV-COMP 2023 setup: BenchExec 3.16 and Goblint svcomp23.

Use SV-COMP time limit for soft exit

It still happens in Dirk's preruns though. It might depend on what exactly Goblint is doing at the time it gets the signal. OCaml's signal handling isn't necessarily immediate. If...

Use SV-COMP time limit for soft exit

SV-COMP 2025 prerun results contain 1298 instances of Goblint TIMEOUT with 960s CPU time, so the issue still remains after the catch-all exception handler fixes.

Use SV-COMP time limit for soft exit

In SV-COMP 2026 preruns there are no results with CPU time over 900s. I have no idea when or why this might've changed then. I was also afraid of how...

valid-memtrack analysis doesn't check sizes, only checks at end & doesn't consider locals

> The usage of free already produces a warning when the offset is non-zero. > Why is this program a problem? We still have the pointer in some way? This...

valid-memtrack analysis doesn't check sizes, only checks at end & doesn't consider locals

> The problem is constructing the pointer already. And precisely constructing that pointer is the valid-memtrack violation by going out of the allowed bound. The valid-memtrack property definition is updated...

valid-memtrack analysis doesn't check sizes, only checks at end & doesn't consider locals

I started looking into it, thinking perhaps one could just reuse bounds checking from memOutOfBounds analysis, but that lead me to another issue: memLeak analysis only looks for reachable things...

valid-memtrack analysis doesn't check sizes, only checks at end & doesn't consider locals

All the points above have nothing to do with finiteness though. The reason valid-memtrack is an interesting property (not just in SV-COMP, but that's also what Valgrind and LeakSanitizer analyze)...

def_exc bounds refinement is asymmetric

This is somehow related to PR #1723, although it doesn't need such a generalization. Still, the behavior of `IntDomain0.Size.min_range_sign_agnostic` is weird and seems to cause the asymmetric bounds.