0000537: unique file handles

Mercury Bugs - mercury
View Issue Details

ID	Project	Category	View Status	Date Submitted	Last Update
0000537	mercury	Feature Request	public	2021-08-31 20:40	2021-08-31 20:40

Reporter	zs
Assigned To
Priority	low	Severity	feature	Reproducibility	N/A
Status	new	Resolution	open
Platform		OS		OS Version
Product Version
Target Version		Fixed in Version

Summary	0000537: unique file handles
Description	At 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.
Tags	No tags attached.
Relationships
Attached Files

There are no notes attached to this issue.