FStarLang/karamel

Kremlin inlining issue

wintersteiger opened this issue · 0 comments

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.