Mercury Bugs - mercury
View Issue Details
0000537mercuryFeature Requestpublic2021-08-31 20:402021-08-31 20:40
Reporterzs 
Assigned To 
PrioritylowSeverityfeatureReproducibilityN/A
StatusnewResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000537: unique file handles
DescriptionAt the moment, once you open a file and get a file handle, you can
(try to) perform operations using that handle even after the handle
is closed.

We could add a new module to the library, called maybe uio.m,
where an open of a file gives you a *unique* file handle. Every
operation then takes a di,uo pair of the relevant kind of unique
file handle ({in,out}put, {text,binary}, and gives you back the
same handle you gave it. The exception is the close operation,
which takes a di file handle. This way, mode analysis could guarantee
the absence of operations on closed files.

The implementation would be simple, using type casts to the existing
file handle types with foreign code, followed by a call to the
equivalent predicate in io.m.

We would need some mechanism to detect the duplication of these unique
file handles during forks and fork-like operations, but that shouldn't
be too hard.
TagsNo tags attached.
Attached Files

There are no notes attached to this issue.

Issue History
2021-08-31 20:40zsNew Issue