How to consume a FILE_v?

[Chris Double]

In the following code I open a file with 'fopen', and later close it
with 'fclose1':

val fp = fopen(argv[0], file_mode_r)
val () = assertloc(FILEptr2ptr(fp) > 0)
val (pf_r | r) = fclose1(fp)
if r < 0 then let
prval Some_v pf = pf_r
prval () = __destroy(pf) where { extern prfun __destroy
{l:addr}{m:fm} (pf: FILE_v(l,m)): void }
in () end
else let
prval None_v () = pf_r
in () end

In the error handling part of the 'if' I get a FILE_v - to consume it
I've created a local proof function - is this the right approach? What
can I actually do with that FILE_v proof? I couldn't find any obvious
function that removes it. Or am I handling the 'flcose1' completely
wrong?

--
http://bluishcoder.co.nz

[gmhwxi]

What you did is fine.

Often one has to have some knowledge of the cause of the error
in order to properly handle it.

Fclose sets the errno EBADF (bad file descriptor) if it fails. But this
can't really happen as FILE_v is already attached to the passed pointer.
I would just do:

val () = assertloc(r = 0) // fclose is expected to succeed