aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* test/*/Makefile: suppress dependencies on ../../ccompXavier Leroy2017-09-112-6/+6
| | | | | Not very useful in practice (make clean is generally done before make all) and problematic under Cygwin where ../../ccomp is really ../../ccomp.exe
* Makefile: chmod a-w instead of chmod -wXavier Leroy2017-09-111-1/+1
| | | | | The latter, in conjunction with some values of the umask, gives weird messages "new permissions are ... not ...".
* Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-282-16/+6
| | | | | Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert. Remove 'Require Export' from Clightdefs as suggested in issue #199.
* For running tests with the interpreter, use the correct -stdlib optionXavier Leroy2017-08-281-3/+2
| | | | Otherwise the interpreter uses the system's header files instead of CompCert's. This can lead to mismatches e.g. on the definition of wchar_t.
* test/compression: use unique temporary files for testingXavier Leroy2017-08-271-7/+7
|
* riscV/Conventions1: in 32-bit mode, wrong size for stack-allocated arguments ↵Xavier Leroy2017-08-261-2/+5
| | | | | | of type Tfloat A default size of 1 was used instead of the correct "typesize ty".
* riscV/Machregs: no printable name was associated to register X31Xavier Leroy2017-08-261-1/+1
|
* test/ : stop at first error in "make all"Xavier Leroy2017-08-261-1/+1
|
* test/: add a CCOMPOPTS make variable to pass additional compile-time flagsXavier Leroy2017-08-265-5/+5
| | | | E.g. "-Os" for testing in "optimize for size" mode, or "-mthumb" for testing ARM in Thumb2 mode.
* Reduce the running times of the tests in test/cXavier Leroy2017-08-2630-87/+75
| | | | Running times were too long when executed on low-end ARM or PowerPC hardware, or under QEMU emulation.
* Prefixed runtime functions.Bernhard Schommer2017-08-2560-269/+269
| | | | | | | The runtime functions are prefixed with compcert in order to avoid potential clashes with runtime/builtin functions of other compilers. Bug 22062
* Document -finline in help.Bernhard Schommer2017-08-241-0/+1
|
* Fixed typo.Bernhard Schommer2017-08-241-1/+1
|
* Extended support for the nostartfiles option.Bernhard Schommer2017-08-231-6/+11
| | | | | For dcc one needs to pass -Ws to tell the linker that it should not link the default startfiles.
* ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudo, continuedXavier Leroy2017-08-221-1/+2
| | | | A 16-bit "nop" is needed because in "add pc, r14" pc reads as the address of the add instruction plus 4, and "add pc, r14" has a 16-bit encoding.
* ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudoXavier Leroy2017-08-222-6/+7
| | | | It is also easier to recognize than the old one for binary analysis tools.
* Issue P #25: make sure sizeof(long double) = sizeof(double) in all contexts.Xavier Leroy2017-08-222-10/+12
|
* Update documentation index for release 3.1v3.1Xavier Leroy2017-08-181-23/+17
|
* Merge remote-tracking branch 'private/master'Xavier Leroy2017-08-188-91/+201
|\
| * Merge pull request #22 from AbsIntPrivate/arm_large_offsetsXavier Leroy2017-08-188-91/+201
| |\ | | | | | | Issue #P18: handle large offsets when accessing return address and back link in the stack frame
| | * ARM: tweak stack layout so that back link and return address are lowerXavier Leroy2017-08-171-37/+34
| | | | | | | | | | | | This reduces the chances that back link and return address cannot be saved by a single str instruction. We generate correct code for the overflow case, but the code isn't very efficient, so let's make it uncommon.
| | * ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-176-47/+88
| | | | | | | | | | | | | | | | | | Saving the return address register (R14) in the function prologue can be done either with a single "str" instruction if the offset is small enough, or by constructing the address using the R12 register as a temporary then storing with "str" relative to R12. R12 can be used as a temporary because it is marked as destroyed at function entry. We just need to tell Asmgen.translcode whether R12 still contains the back link left there by Pallocframe, or R12 was trashed. In the latter case R12 will be reloaded from the stack at the next Mgetparam instruction.
| | * Asmgenproof0: some more useful lemmasXavier Leroy2017-08-171-0/+29
| | | | | | | | | | | | Next commit uses those lemmas in the ARM port.
| | * ARM: Generate Pcfi_rel_offset directives directly from AsmgenXavier Leroy2017-08-174-12/+17
| | | | | | | | | | | | This is what we do for PowerPC and is more resilient to changes in code generation. We need to give Pcfi_rel_offset a dynamic semantics, but that's just a no-op.
| | * Push correct registerMichael Schmidt2017-08-021-1/+1
| | |
| | * Improve stack offset addressingMichael Schmidt2017-08-025-35/+73
| | | | | | | | | | | | Functions which require large amounts of stack for spilling and/or arguments for function calls lead to stackframe offsets that exceed the 12bit limit of immediate constants in ARM instructions. This patch fixes the stack-offsets in the function prolog/epilog.
* | | configure: Wording and formatting of the Skylake/OCaml warningXavier Leroy2017-08-181-2/+3
| | |
* | | Update Changelog in preparation for release 3.1Xavier Leroy2017-08-181-2/+8
|/ /
* / Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-153-13/+34
|/ | | | | | The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196. The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-07-311-1/+3
|\
| * Mention rv32- and rv64- configurations in the help messageXavier Leroy2017-07-311-0/+2
| | | | | | | | These are the configurations for the new RISC-V port.
| * Accept Coq version 8.6.1 as supportedXavier Leroy2017-07-311-1/+1
| | | | | | | | 8.6.1 works just fine with the current CompCert.
* | Warning for Skylake/Kabylake systems.Bernhard Schommer2017-07-311-0/+4
|/
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-07-271-20/+27
|\
| * use TMPDIR also for asm-cfi testMichael Schmidt2017-07-271-5/+5
| |
| * generalize test for compiler optionsMichael Schmidt2017-07-271-15/+22
| |
* | Update Changelog with news since release 3.0.1Xavier Leroy2017-07-271-4/+29
|/
* Integrated fixup code in estimated size.Bernhard Schommer2017-07-261-0/+3
| | | | | | | 12 was a too small overaproximation for call which require fixup code for arguments and result. The new constant is 72, which consists of 4 for the branch instruction, 16 * 4 for the arguments and 4 for the result.
* Added annot to json dump.Bernhard Schommer2017-07-241-3/+20
|
* Print_annot should produce a string.Bernhard Schommer2017-07-195-40/+54
|
* No verbose debug info in default mode.Bernhard Schommer2017-07-141-5/+17
| | | | | | We don't need verbose debug for the assembler. The verbose debug information should only be printed if assembler files are generated.
* Update documentation entry point for release 3.0 (retroactively)Xavier Leroy2017-07-131-5/+8
| | | | Some modules new in 3.0 were not mentioned.
* Constprop strength reduction (#17)Bernhard Schommer2017-07-124-16/+325
| | | | | | | PowerPC port: add strength reduction for 64-bit operations * Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748) * Moved shru_rolml proof to Values.
* SimlLocals.Sdebug_var: wrong type for 64-bit platformsXavier Leroy2017-07-091-1/+1
| | | | | | Fixes: Github issue #190. Tint was used instead of the correct Tptr.
* Add a -ignore-coq-version flag to configure (continued)Xavier Leroy2017-07-061-2/+2
| | | | These Coq people have version "numbers" that look nothing like numbers, such as "trunk". Also, they didn't test their pull request #188. Fixing this.
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-0618-99/+283
| | | | | | | | - Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-0629-37/+211
| | | | | | This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses. Current status: x86 port only, the only new addressing mode handled is reg + offset.
* Issue #16P: wrong rlwinm instruction generated by constant propagationXavier Leroy2017-07-053-13/+30
| | | | This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-07-051-0/+30
|\
| * Merge pull request #14 from AbsIntPrivate/configure_no_pieMichael Schmidt2017-07-051-0/+30
| |\ | | | | | | Extension of configure for issue #189
generated by cgit (git 2.34.1) at 2024-07-02 18:38:30 +0000