Simmo Saan

This is a point in #1722. For example, this will produce a witness with invariants containing our fictitious `__annonCompField` offsets: ```console ./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/unreach-call.prp --set exp.architecture 64bit...

For SV-COMP correctness witnesses we only output loop invariants. For goto-based loops, we output nothing. Following Matthias Heizmann's proposal, we should also output location invariants at labels. So goto-based loops...

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

8

I started looking into allowing our SV-COMP valid-memtrack analysis to still consider one-past-end pointers to track memory for the rule change: https://gitlab.com/sosy-lab/sv-comp/bench-defs/-/merge_requests/471. However, I am really confused because the `memLeak`...

Inspired by https://github.com/goblint/analyzer/issues/1710#issuecomment-2717951685, I wondered what invariants C2PO analysis even generates. Turns out, none! Which is surprising, because it does implement the `Invariant` query. I have no idea what's happening...

In #1849 our relational domains produce a witness invariant ```c (long long )i >= (long long )\at(i, AnyPrev) + 1LL ``` This is a transition invariant, but that's actually beside...

`exp.volatiles_are_top` and `exp.globs_are_top` are only considered by base analysis

1

These options are only considered by the base analysis. All other analyses (especially relational) are unaffected and still assume non-top values, which defeats the point of these options. Now thinking...

`var_eq` doesn't remove unreachable variables in `enter`

2

Here's `enter` for `var_eq` analysis: https://github.com/goblint/analyzer/blob/5614dd34bb45e3bb7f960bfddd512d00106aa4aa/src/analyses/varEq.ml#L412-L430 The comment claims it tries to remove unreachable variables but nowhere does it actually do that. This means that the analysis keeps around equalities...

def_exc bounds refinement is asymmetric

1

This is something I found out while tracing various versions during PR #1756 and is added as a test there: ```c if (-10

The following obscure examples are from https://blog.aaronballman.com/2013/06/interesting-note-about-the-sizeof-operator/. ```c #include int main( void ) { int a = 12; int b = sizeof( ++a ); printf( "%d\n", a ); return 0;...

As I noted in #1804: > domain tests don't check the overflow flags of abstract operator results. Moreover, when the concrete operator calculates the overflowed value, it's forced into bounds...