Kremlin inlining issue
wintersteiger opened this issue · 0 comments
wintersteiger commented
Removing the inline_for_extraction
from hcpy
here: https://github.com/project-everest/hacl-star/blob/cwinter_merkle_hashes/secure_api/merkle_tree/MerkleTree.Low.Datastructures.fst#L189 makes kremlin produce (hcpy(hsz), (void*)0)
instead of hcpy(hsz)
, i.e. the result is overwritten by a null pointer.