law validate_mem_init

bend-osdev-bpf@0.1.0.0 · LAWS.bend:317

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/validate.bend as V

317# scratch memory read before it is written: refused by default, on every
318# path (here the jump past the store), and allowed by the permissive options
319law validate_mem_init:
320  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrMemInit{0n}} : Result<&2, &2, I.BpfError, Unit>}