Simmo Saan

Static function pointers for stubs and inverted stubs

1

## Use case Currently it is possible to use `foreign` to declare C functions that take function arguments via `static_funptr`. In various places (including issues of this repository) it is...

Unfortunately there are many users of this action, who use it via `setup-ocaml@master` and have done so from the v1 days. Although v2 was breaking and renamed `ocaml-version` → `ocaml-compiler`,...

Support opam lock file

4

I'm trying to set up a workflow that uses the dependencies specified by an `.opam.locked` file in the repository instead of using the unlocked `.opam` file directly. However this silently...

Remove `ID.is_bool` and `ID.is_int`

1

This fixes an assert failing in `sv-benchmarks/c/recursive/MultCommutative-2` here: https://github.com/goblint/analyzer/blob/a4e917f86c983d7c97138364b07e031a7715e3d5/src/analyses/base.ml#L2216-L2220 The problem was that `ID.is_bool value = true` but `ID.to_bool = None`, which of course shouldn't happen. The offending `value` is...

Optimize and refactor "Hoare" domains

11

Related to issues #101 and #803. ### TODO - [x] Benchmark on sv-benchmarks. - [x] Check performance on SQLite. - [x] Fix termination issue when `SetDomain.Joined` is used inside `AddressDomain`?...

Unassume witness invariants during solving

1

This PR adds an unassume analysis, which loads a YAML witness before solving and emits `Unassume` events during the analysis at nodes which have invariants. Both base, apron and var_eq...

Migrate from CIL's `Pretty` to OCaml's `Format`

3

In #210 it came up multiple times that OCaml's standard [`Format`](https://ocaml.org/api/Format.html) module could replace [`Pretty`](https://people.eecs.berkeley.edu/~necula/cil/api/Pretty.html) from CIL with additional benefits: 1. It's maintained in OCaml's standard library while `Pretty` isn't...

As discussed in GobCon, this would be something to somewhat limit the large number of invariants we generate. Since accesses are to lvalues, not just variables, this also has lvalue...

Use Cram for tests

4

Here's a wild idea I toyed with, which we can either make complete or just close this PR. Basically, dune's Cram tests are designed for testing executables and could have...

This ~~hopefully~~ fixes _all_ remaining `ERROR (verify)` results on sv-benchmarks ([Full table](https://goblint.cs.ut.ee/results/85-all-fast-hoaredomain-after-bool-range/table-generator.table.html#/table)). It is on top of #809 since that causes significant changes to `ERROR (verify)` results. ### Changes 1....