truncate extension sometimes extends with file names instead of zeros about fscq HOT 4 CLOSED

Thanks; I will take a look. Sounds like we might have gotten the spec wrong.

from fscq.

Indeed, we proved the wrong spec about truncate -- the FS.file_set_sz_recover_ok theorem. The implementation just sets the length field but doesn't do anything useful with the data blocks (and the theorem just talks about the file metadata). This is because we wrote this operation before implementing byte-level file contents, and forgot to go back and fix it. The truncate operation should instead call something like ByteFile.grow_file, but passed through the tree abstraction in DirTree.v. I'll try to fix this soon.

from fscq.

This should be fixed in c679921.

Incidentally, your test case didn't compile on a strict C compiler because it was missing a second argument to creat(). :-)

from fscq.

This issue is closed, but I just need to add that this problem was detected by David Sheets (dsheets) using SibylFS (David is one of the authors on the SibylFS paper). This is part of the "evidence trail" for the UK "research excellence framework".

from fscq.