karamel icon indicating copy to clipboard operation
karamel copied to clipboard

Kremlin inlining issue

Open wintersteiger opened this issue 5 years ago • 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.

wintersteiger avatar Feb 21 '20 17:02 wintersteiger