"Permission denied" during copying of result files

[PhilippWendler]

There are two cases where a warning message of the form Could not retrieve output file '...': [Errno 13] Permission denied: ... is printed by BenchExec:

1. If the tool produces a result file without write permission.
2. If the tool produces a result file without read permission, or directories without execute permission.

Case 1. only happens because when copying output files we actually perform a move operation:

benchexec/benchexec/containerexecutor.py

Lines 1219 to 1222 in 033b38c

	# move is more efficient than copy in case both abs_file and target
	# are on the same filesystem, and it avoids matching the file again
	# with the next pattern.
	shutil.move(abs_file, target)

The file is still copied correctly. We should fix that and do not print a useless warning.

Case 2 is more interesting. If a tool creates a non-readable file, BenchExec could still make the file readable (we have that permission) and then copy it. Or we could keep the existing behavior.
@MartinSpiessl @dbeyer Any thoughts on this last point? What would you prefer? I tend towards adding the missing permission and copying the file.

[MartinSpiessl]

I would say it is a file that was generated, so it should be collected.

[Vishnurr2k01]

is this issue fixed ?

[PhilippWendler]

No, nothing has happened so far in this regard.