Simmo Saan

Display device info and status. Allow configuration.

A la https://github.com/Denton-L/based-connect.

Failed to verify: pthread_create(&m_thread_id, NULL, &thread_func, this) == 0

8

I experimented around with this and with nontrivial examples I'm getting an error: > Failed to verify: pthread_create(&m_thread_id, NULL, &thread_func, this) == 0 Example of code causing that: ```lisp (declare-const...

This depends on #61 being merged, the PR diff currently isn't nice, but a nicer diff can be seen here: https://github.com/sim642/sv-witnesses/compare/yaml-schema...goblint:sv-witnesses:flow_insensitive_invariant. While loop invariants and location invariants (#62) are associated...

This adapts #59 on top of #61. Since this depends on #61 being merged, the PR diff currently isn't nice, but a nicer diff can be seen here: https://github.com/sim642/sv-witnesses/compare/yaml-schema...goblint:sv-witnesses:location_invariant. ###...

Combined schema for YAML witnesses

6

### Changes 1. Replace `loop_invariant` schema with a combined schema that also specifies `loop_invariant_certificate`. 2. Add descriptions to schema. 3. Extract reusable `$defs` in schema to simplify new entry type...

Publish Z_mlgmpidl module on opam

2

As pointed out in #118, the `Z_mlgmpidl` module present here can be used, but it's not built or packaged on opam. Since it works, it shouldn't hurt to also publish...