You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When a tool truncates the file descriptors that it has for stdout and stderr, this leads to truncation of the log file with the output. So a tool can undo output that it has previously written, and it can remove and overwrite the first few lines of the log that are written by BenchExec (with the command line).
While we could argue that making a tool to remove its own output would be acceptable, it should not be able to overwrite the lines that BenchExec produces.
This can even happen unintentionally if /dev/stdout or /dev/stderr is used for output redirection with > instead of >>.
The file content is deleted completely, and echo_stderr1 is written to the beginning of the file.
echo_stdout2 is appended to the file, so it appears after the position where the output from 2. ended. The hole in the file between the output from 3. and 4. is filled with null bytes.
We could
Use a pipe as target for the output. This would solve this completely, but with overhead during the run.
Add the command line to the log after the run (which involves copying the whole file). This has no overhead during the run but does not solve the tool overwriting its own output and the null bytes.
Investigate whether there is some option that prevents a file descriptor from being truncated (maybe chattr +a helps).
The text was updated successfully, but these errors were encountered:
When a tool truncates the file descriptors that it has for
stdout
andstderr
, this leads to truncation of the log file with the output. So a tool can undo output that it has previously written, and it can remove and overwrite the first few lines of the log that are written by BenchExec (with the command line).While we could argue that making a tool to remove its own output would be acceptable, it should not be able to overwrite the lines that BenchExec produces.
This can even happen unintentionally if
/dev/stdout
or/dev/stderr
is used for output redirection with>
instead of>>
.Example:
The following happens:
echo_stdout1
is appended.echo_stderr1
is written to the beginning of the file.echo_stdout2
is appended to the file, so it appears after the position where the output from 2. ended. The hole in the file between the output from 3. and 4. is filled with null bytes.We could
chattr +a
helps).The text was updated successfully, but these errors were encountered: