search

project-everest / mitls-fstar

Verified implementation of TLS 1.3 in F*
https://www.mitls.org
Other
173 stars 16 forks source link

Risk of stack overflow while using buffer_utils_memset #166

Closed msprotz closed 6 years ago

msprotz commented 7 years ago

@BarryBo points out that Buffer.Utils.memset is not tail-recursive (and there's a comment to that effect in the source tree). https://github.com/FStarLang/kremlin/blob/master/kremlib/C.Loops.fst has combinators for writing functions that are actual for-loops in the extracted C code.

CC @ad-l @s-zanella

BarryBo commented 6 years ago

Kremlin's tail-recursion optimization turned this into a nice for() loop a while back.