Skip to content

gen_heap: expose that inG identities are preserved

Ralf Jung requested to merge ralf/gen-heap-names into master

Perennial currently has to re-prove gen_heap_init because it needs to know that the inG instances stay the same when turning gen_heapPreG into gen_heapG. This comes from the fact that Perennial needs to instantiate the heap multiple times during an execution to account for crashes: gen_heap_init is called after each crash to pick new ghost name instances.

Merge request reports