Revision 10dabb73a66ea8e85408542abc7710ece7c76e96 authored by Jonathan Protzenko on 03 December 2019, 20:23:07 UTC, committed by Jonathan Protzenko on 03 December 2019, 20:26:28 UTC
1 parent 2d7a98b
Lib.PrintBuffer.fsti
module Lib.PrintBuffer
open Lib.IntTypes
open Lib.Buffer
open FStar.HyperStack.All
val print_bytes:
len: size_t
-> buf: lbuffer uint8 len ->
Stack unit
(requires (fun h -> live h buf))
(ensures (fun h0 _ h1 -> modifies0 h0 h1))
val print_compare:
len: size_t
-> buf0: lbuffer uint8 len
-> buf1: lbuffer uint8 len ->
Stack unit
(requires (fun h -> live h buf0 /\ live h buf1))
(ensures (fun h0 _ h1 -> modifies0 h0 h1))
val print_compare_display:
len: size_t
-> buf0: lbuffer uint8 len
-> buf1: ilbuffer uint8 len ->
Stack unit
(requires (fun h -> live h buf0 /\ live h buf1))
(ensures (fun h0 _ h1 -> modifies0 h0 h1))
val result_compare_display:
len: size_t
-> buf0: lbuffer uint8 len
-> buf1: ilbuffer uint8 len ->
Stack bool
(requires (fun h -> live h buf0 /\ live h buf1))
(ensures (fun h0 _ h1 -> modifies0 h0 h1))
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...