Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Add some tests | nicolas.nardino | 2021-06-08 | 2 | -0/+130 |
| | |||||
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1 | Cyril SIX | 2021-06-01 | 35 | -157/+89 |
|\ | |||||
| * | Compatibilité Coq 8.13 | David Monniaux | 2021-04-28 | 2 | -0/+0 |
| | | |||||
| * | Merge branch 'kvx-work' of ↵ | Léo Gourdin | 2021-04-22 | 3 | -0/+15 |
| |\ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work | ||||
| | * | rm spurious files | David Monniaux | 2021-04-12 | 39 | -1705/+0 |
| | | | |||||
| | * | test profiling | David Monniaux | 2021-04-12 | 42 | -0/+1720 |
| | | | |||||
| * | | moving my tests | Léo Gourdin | 2021-04-22 | 26 | -157/+0 |
| |/ | |||||
| * | Merge branch 'riscv-work' into kvx-work | Léo Gourdin | 2021-04-09 | 2 | -0/+13 |
| |\ | |||||
| | * | Removing expansions from Asmgen | Léo Gourdin | 2021-04-09 | 1 | -0/+6 |
| | | | |||||
| | * | fp test | Léo Gourdin | 2021-03-10 | 1 | -0/+7 |
| | | | |||||
| * | | adding test for load replacement on a64 | Léo Gourdin | 2021-03-29 | 4 | -0/+61 |
| |/ | |||||
* | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵ | Cyril SIX | 2021-06-01 | 3 | -1/+24 |
| | | | | | | | | cfrontend/C2C.ml | ||||
* | | Updating varargs2 results for kvx | Cyril SIX | 2021-06-01 | 1 | -0/+1 |
| | | |||||
* | | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 12 | -420/+604 |
|\ \ | |/ |/| | | | | | | | | | | | | | 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 | ||||
| * | "macosx" is now called "macos" | Xavier Leroy | 2021-01-18 | 1 | -1/+1 |
| | | | | | | | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos". | ||||
| * | Remove regression/interop1 test | Xavier Leroy | 2021-01-18 | 4 | -417/+1 |
| | | | | | | | | Now subsumed by the tests in abi/ | ||||
| * | Testing calling conventions and interoperability with another C compiler | Xavier Leroy | 2021-01-18 | 5 | -1/+583 |
| | | | | | | | | Using a combination of fixed and randomly-generated function signatures. | ||||
| * | RISC-V: fix FP calling conventions | Xavier Leroy | 2021-01-14 | 2 | -5/+5 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a follow-up to e81d015e3. In the RISC-V ABI, FP arguments to functions are passed in integer registers (or pairs of integer registers) in two cases: 1- the FP argument is a variadic argument 2- the FP argument is a fixed argument but all 8 FP registers reserved for parameter passing have been used already. The previous implementation handled only case 1, with some problems. This commit implements both 1 and 2. To this end, 8 extra FP caller-save registers are used to hold the values of the FP arguments that must be passed in integer registers. Fixup code moves these FP registers to integer registers / register pairs. Symmetrically, at function entry, the integer registers / register pairs are moved back to the FP registers. 8 extra FP registers is enough because there are only 8 integer registers used for parameter passing, so at most 8 FP arguments may need to be moved to integer registers. | ||||
| * | RISC-V: wrong fixup code generated for vararg calls with fixed FP args | Xavier Leroy | 2021-01-10 | 2 | -0/+17 |
| | | | | | | | | | | | | | | | | | | This is a follow-up to 2076a3bb3. Integer registers were wrongly reserved for fixed FP arguments, causing variadic FP arguments to end up in the wrong integer registers. Added regression test in test/regression/varargs2.c | ||||
* | | example of cmov | David Monniaux | 2021-02-02 | 1 | -0/+28 |
| | | |||||
* | | cmov on integers | David Monniaux | 2021-02-02 | 1 | -0/+22 |
| | | |||||
* | | Conditions now propagated by CSE3 | David Monniaux | 2021-01-20 | 1 | -0/+11 |
|\ \ | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work | ||||
| * | | redundant tests | David Monniaux | 2020-12-09 | 1 | -0/+11 |
| | | | |||||
* | | | a slightly different matrix product | David Monniaux | 2021-01-14 | 1 | -0/+24 |
| | | | |||||
* | | | generate a matrix product with many temporaries | David Monniaux | 2021-01-14 | 1 | -0/+20 |
| | | | |||||
* | | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2021-01-07 | 1 | -0/+14 |
|\ \ \ | |||||
| * | | | Removing Yarpgen test 89 | Cyril SIX | 2021-01-07 | 1 | -0/+14 |
| |/ / | | | | | | | | | | Issue #232 | ||||
* | | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 16 | -115/+871 |
|\| | | |||||
| * | | Fixing test/regression for KVXv3.8_kvx | Cyril SIX | 2020-12-07 | 2 | -0/+393 |
| | | | |||||
| * | | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 11 | -13/+380 |
| |\ \ | | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure | ||||
| * \ \ | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 15 | -115/+478 |
| |\ \ \ | | | |/ | | |/| | |||||
| | * | | Better "make clean" | Xavier Leroy | 2020-11-01 | 1 | -1/+1 |
| | | | | |||||
| | * | | Test clightgen with -short-idents and -normalize options | Xavier Leroy | 2020-09-22 | 1 | -0/+6 |
| | | | | | | | | | | | | | | | | Use different combination of options for different test files. | ||||
| | * | | Support the use of already-installed MenhirLib and Flocq libraries | Xavier Leroy | 2020-09-21 | 1 | -2/+6 |
| | | | | | | | | | | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib. | ||||
| | * | | Add test for __builtin_sqrt and __builtin_fabsf | Xavier Leroy | 2020-07-27 | 2 | -0/+7 |
| | | | | |||||
| | * | | Refactor regression testing of built-in functions | Xavier Leroy | 2020-07-27 | 13 | -110/+447 |
| | | | | | | | | | | | | | | | | | | | | | | | | Share the testing code for built-in functions that are available on all target platforms. Improve testing of __builtin_clz* and __builtin_ctz* | ||||
| | * | | Improve portability of the test for annotations inclightgen | Xavier Leroy | 2020-06-05 | 2 | -0/+4 |
| | | | | | | | | | | | | | | | | __builtin_ais_annot is not supported for macOS nor for Cygwin. | ||||
| | * | | clightgen: fix the printing of annotations | Xavier Leroy | 2020-06-05 | 1 | -0/+6 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The printing of EF_annot and EF_annot_val was missing the extra "kind" parameter introduced in commit 6a010b4. Also: the automatic translation of annotations into Coq assertions was confusing and prevented other uses of __builtin_annot statements in conjunction with clightgen. I believe it was never used. This commit removes this translation. Closes: #360 | ||||
* | | | | Merge branch 'kvx-test-prepass' of ↵ | David Monniaux | 2020-11-27 | 11 | -13/+380 |
|\ \ \ \ | | |_|/ | |/| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass | ||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 2 | -0/+256 |
| |\| | | |||||
| * | | | turn on cache emulation | David Monniaux | 2020-10-19 | 1 | -9/+9 |
| | | | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 2 | -1/+29 |
| |\ \ \ | |||||
| * \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-02 | 6 | -17/+29 |
| |\ \ \ \ | |||||
| * | | | | | rules.mk for zigzag | David Monniaux | 2020-09-24 | 1 | -7/+7 |
| | | | | | | |||||
| * | | | | | Merge remote-tracking branch 'origin/kvx-work' into ↵ | David Monniaux | 2020-09-05 | 4 | -9771/+45 |
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | mppa-RTLpathSE-verif-hash-junk iMe | ||||
| * | | | | | | -ftracelinearize | David Monniaux | 2020-07-30 | 1 | -12/+12 |
| | | | | | | | |||||
| * | | | | | | Merge remote-tracking branch 'origin/kvx-work' into ↵ | David Monniaux | 2020-07-30 | 1 | -2/+3 |
| |\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | mppa-RTLpathSE-verif-hash-junk | ||||
| * \ \ \ \ \ \ | Merge branch 'mppa-RTLpathSE-verif-hash-junk' of ↵ | David Monniaux | 2020-07-27 | 4 | -0/+188 |
| |\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk | ||||
| | * | | | | | | | test for speculative load | David Monniaux | 2020-07-26 | 2 | -0/+19 |
| | | | | | | | | | |||||
| | * | | | | | | | simplified | David Monniaux | 2020-07-26 | 1 | -4/+2 |
| | | | | | | | | |