Moved file functions in own file. #169
Conversation
The file functions are moved into an own library file. The temp_file function now registers a delete function at exit. This avoids the double check for temp files in driver. Currently unused is the input_file type and functions since most functions using this are affected by the other changes in PR #158 and changing them would result in doubled work. Bug 20521
|
Just had a quick look, need to read again. +1 for the temporary files with automatic removal at exit, that simplifies things nicely. Less sure about the other changes. Probably I should look at #158 to see where you're going with the |
|
The input file is used to simplify the whole handling of suffix cutting etc. and it also includes the check whether the file exists or not. |
|
That's one thing I wanted to mention in a future code review: checking that a file exists at time T gives no guarantee that the file can be read later, i.e. that open_in{_bin} will succeed. (File could have been removed, or could have the wrong permissions, etc.) |
|
The main reason for checking this in CompCert is to avoid for passing non-existing files to the external tools, we could extend the check to test whether the file has the right permissions. |
|
I will rebase this and add a check for file permissions etc. |
Following the gnu Makefile Conventions the variable $(DESTDIR) should be prepended to all installation commands. This allows staged installs.
* CompatibleCompCert: (75 commits) Coq 8.9.1 support Csyntax.v: Fix a typo in a documentation comment (AbsInt#292) Add a check for the args of unprototyped calls. Provide a default "select" operation for the RiscV port Implement a `Osel` operation for ARM Implement a `Osel` operation for x86 Emulate the "isel" instruction on non-EREF PPC processors Implement a `Osel` operation for PowerPC Give a semantics to the Pisel instruction Support a "select" operation between two values PowerPC: make sure evaluation of conditions do not destroy any register Prepend $(DESTDIR) to the installation target (AbsInt#169) Reworked elaboration of declarations/definitions. Added options -fcommon and -fno-common (AbsInt#164) Change to AbsInt version string. Check for reserved keywords. Fix various scoping issues (AbsInt#163) Ensure flushing of the error formatter. Expand the responsefiles earlier Check for alignment of command-line switches. ... # Conflicts: # configure # flocq/Calc/Operations.v # flocq/Core/Defs.v # flocq/IEEE754/Bits.v # flocq/Prop/Sterbenz.v
The file functions are moved into an own library file. The
temp_file function now registers a delete function at exit. This
avoids the double check for temp files in driver.
Currently unused is the input_file type and functions since most
functions using this are affected by the other changes in PR #158
and changing them would result in doubled work.
Another prequisite for the option pipe PR #158