| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
cfrontend/C2C.ml
|
|\ \
| |/
|/|
| |
| |
| |
| |
| |
| | |
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
|
| |
| |
| |
| |
| | |
The configure script still accepts "macosx" for backward compatibility,
but every other part of CompCert now uses "macos".
|
| |
| |
| |
| |
| | |
This commit adds support for macOS (and probably iOS) running on
AArch64 / ARM 64-bit / "Apple silicon" processors.
|
| | |
|
|\ \
| | |
| | |
| | | |
Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
|\ \ \ \
| | |/ /
| |/| | |
|
| |\ \ \
| | | |/
| | |/| |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Outside of -interp mode, -main has no (known) effect but could be
confused for a linker option that sets the program's entrypoint, say.
It's safer to reject the option.
|
| |\ \ \
| | | |/
| | |/|
| | | |
| | | |
| | | | |
Conflicts:
Makefile
configure
|
| |\ \ \
| | | |/
| | |/| |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function.
This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option.
The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
|
| | | |
| | | |
| | | |
| | | | |
It is specific to AbsInt's commercial version of CompCert.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | | |
This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The version string dumped in the file should be the same as the version
string printed by `-version`. The option is also not printed by `-help`
since it is for internal use only.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The Commandline module is reusable in other projects, and its license
(GPL) allows such reuse, so its natural place is in lib/ rather
than in driver/
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The list of reserved_registers is never reset between the compilation of
multiple files. Instead of storing them in IRC they are moved in the
CPragmas file and reset in the a new reset function for Cpragmas whic is
called per file.
|
| |_|/
|/| | |
|
|\ \ \ |
|
| |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Previously, the elimination of useless conditions done in the 2nd pass of the tunneling
introduced some new "nop" instructions that were not eliminated.
This commit solves this issue by anticipating the elimination of conditions in the 1st pass
of the tunneling, the 2nd pass being unchanged.
In case of cycles in the CFG, the full elimination of useless conditions may require several
iterations in the 1st pass. Moreover, in the simulation proof, the measure counting the number of
eliminated steps from each node, needs to be adapted according to the modifications on the 1st pass.
Hence, this measure results from a quite complex fixpoint computation: proving its properties
would be very difficult.
This leads us to introduce an oracle, implementing the first pass and producing the expected
measure. A certified verifier directly checks that the measure provided by the oracle
satisfies the properties expected by the simulation proof.
Introducing this oracle/verifier pair has here the following advantage:
- the proof is simpler than the original one (e.g. having a certified union-find structure
is no more necessary for this pass).
- the oracle is very efficient, by using imperative data-structure to compute memoized
fixpoints.
At runtime, the overhead induced by the verifier computations (and the actual computation of
the measure) seems largely compensated by the gains obtained through the imperative oracle.
|
|\| | |
|
| | | |
|
|\| | |
|
| | | |
|
| | | |
|
|\| | |
|
| |\ \ |
|
| | | | |
|
|\ \ \ \
| | |/ /
| |/| | |
|
| |/ / |
|
| | | |
|