Dave Thaler

I was thinking it could be done with simple precondition/postcondition invariants like we use now for other things. Not sure why that wouldn't work with existing iteration.

If I replace "# calls" in my proposed invariant above with "# unmatched calls", i.e., reset to 0 on equality of the invariant, then any (forward direction) joins can be...

According to the [man page](https://www.man7.org/linux/man-pages/man7/bpf-helpers.7.html), other eBPF helpers that need this functionality include: * bpf_skc_lookup_tcp -> bpf_sk_release * bpf_sk_lookup_tcp ->bpf_sk_release * bpf_sk_lookup_udp -> bpf_sk_release

The project already exposes prepare_cfg() separately from ebpf_verify_program(). (The check utility calls the former for the "cfg" domain and the latter for the "zoneCrab" domain.) So I think this is...

As @Alan-Jowett noted in #276, the workaround appears to be to compile the program with --target=bpf -mcpu=v1 so that clang doesn't emit the newer instruction types. That said, I suspect...

@Alan-Jowett was this fixed by PR #436? Can this issue be closed now?

> Hi, is there any plan to implement bpf_spin_lock? There is a discussion in https://github.com/vbpf/ebpf-verifier/issues/273

@elazarg Since #298 was merged, is this issue closable now? `bpf_ringbuf_reserve` is marked as `.return_type = EBPF_RETURN_TYPE_PTR_TO_ALLOC_MEM_OR_NULL,`

> There are several check annotations in this PR. What should we do with them? My opinion: they are just warnings in strict mode, not errors so I left them...

https://falco.org/docs/ confirms that Falco as a whole fails the stated requirement that "The project must be using eBPF as its underlying core technology, in other words, a project would lose...