Revision 740e005247abf20870203acc9b37935012e2855a authored by Jonathan Protzenko on 08 June 2020, 20:48:05 UTC, committed by GitHub on 08 June 2020, 20:48:05 UTC
OCaml API: Placeholders for unsupported primitives in Hacl
Lib.Memzero0.fsti
/// Separate module that does not depend on Lib.Buffer to avoid a dependency loop.
module Lib.Memzero0
module B = LowStar.Buffer
/// This variant is polymorphic and is implemented in C.
val memzero: #a:Type0 -> b:B.buffer a -> l:UInt32.t { B.len b == l } -> FStar.HyperStack.ST.Stack unit
(requires fun h -> B.live h b)
(ensures fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1))
Computing file changes ...
