search

mit-pdos / fscq

FSCQ is a certified file system written and proven in Coq
Other
236 stars 21 forks source link

chmod has no effect and does not return an error #5

Closed dsheets closed 5 years ago

dsheets commented 9 years ago

On 27c4078a00b517671163f668ebd644614171d966, when running:

# touch foo
# ls -l foo
-rwxrwxrwx 1 root root 0 Jan  1  1970 foo
# chmod 700 foo
# ls -l foo
-rwxrwxrwx 1 root root 0 Jan  1  1970 foo

an error such as ENOSYS is expected if chmod is not implemented.

zeldovich commented 9 years ago

Pragmatically, this is because we do not handle permissions in the code/theorems, but some applications fail unnecessarily if chmod returns an error. (You are of course correct that this is not legal as far as POSIX goes.)

dsheets commented 9 years ago

Yes, that makes sense. This is perhaps subsumed by #10.