aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| | | * | | | | run yarpgen correctly on armDavid Monniaux2020-03-282-4/+12
| | | |/ / / /
| | | * | | | limit due to stack overflowsDavid Monniaux2020-03-281-1/+1
| | | | | | |
| | | * | | | more fixes for CIDavid Monniaux2020-03-282-3/+3
| | | | | | |
| | | * | | | run yarpgen on other architecturesDavid Monniaux2020-03-281-0/+4
| | | | | | |
| | | * | | | fix inconsistencyDavid Monniaux2020-03-281-8/+7
| | | | | | |
| | | * | | | better assemble with gccDavid Monniaux2020-03-281-2/+3
| | | | | | |
| | | * | | | fix limitxyDavid Monniaux2020-03-281-1/+1
| | | | | | |
| | | * | | | stdlib pathDavid Monniaux2020-03-281-3/+5
| | | | | | |
| | | * | | | run yarpgen test on aarch64David Monniaux2020-03-281-1/+2
| | | | | | |
| | | * | | | some more Makefile fixes (disable cse2 it's too slow)David Monniaux2020-03-281-1/+1
| | | | | | |
| | | * | | | fix targets for proper generationDavid Monniaux2020-03-281-2/+5
| | | | | | |
| | | * | | | fix Makefile (again)David Monniaux2020-03-281-9/+10
| | | | | | |
| | | * | | | fix Makefile for not remaking the generatorDavid Monniaux2020-03-281-13/+13
| | | | | | |
| | | * | | | set up for autogeneration of yarpgenDavid Monniaux2020-03-281-7/+22
| | | | | | |
| | | * | | | cleaner make invocationDavid Monniaux2020-03-281-5/+5
| | | | | | |
| | | * | | | Makefile for CIDavid Monniaux2020-03-282-24/+93
| | | | | | |
| | | * | | | we still need a ppc64 compilerDavid Monniaux2020-03-271-0/+1
| | | | | | |
| | | * | | | disable testing on ppc64David Monniaux2020-03-271-2/+0
| | | | | | |
| | | * | | | +xDavid Monniaux2020-03-271-0/+0
| | | | | | |
| | | * | | | temporarily disable raytracer test on ARMDavid Monniaux2020-03-271-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | https://github.com/AbsInt/CompCert/issues/342
| | | * | | | more configDavid Monniaux2020-03-272-2/+24
| | | | | | |
| | | * | | | fixesDavid Monniaux2020-03-271-1/+0
| | | | | | |
| | | * | | | various fixes for multilibDavid Monniaux2020-03-271-1/+2
| | | | | | |
| | | * | | | fix config for K1C PPC RV32 for CIDavid Monniaux2020-03-272-3/+3
| | | | | | |
| | | * | | | wrong lineDavid Monniaux2020-03-271-1/+1
| | | | | | |
| | | * | | | build and execute tests on other architectures than aarch64David Monniaux2020-03-271-4/+11
| | | | | | |
| | | * | | | call standard qemu not mine!David Monniaux2020-03-271-1/+1
| | | | | | |
| | | * | | | do not use binfmtDavid Monniaux2020-03-271-2/+2
| | | | | | |
| | | * | | | run tests on aarch64David Monniaux2020-03-271-1/+2
| | | | | | |
| | | * | | | disable some testsDavid Monniaux2020-03-271-4/+4
| | | | | | |
| | | * | | | fix issues in Mandelbrot due to modifications in the source codeDavid Monniaux2020-03-271-2/+0
| | | | | | |
| | | * | | | fix broken test MakefileDavid Monniaux2020-03-272-1/+10
| | | |/ / / | | | | | | | | | | | | | | | | | | fix math.h so that it does special things only on K1C
| | | * | | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-264-234/+544
| | | |\| |
| | | | * | RA is preservedDavid Monniaux2020-03-252-18/+36
| | | | | |
| | | | * | proof forwardDavid Monniaux2020-03-251-1/+4
| | | | | |
| | | | * | proof forwardDavid Monniaux2020-03-251-5/+15
| | | | | |
| | | | * | proof forwardDavid Monniaux2020-03-251-6/+24
| | | | | |
| | | | * | Asmgenproof1David Monniaux2020-03-241-1/+3
| | | | | |
| | | | * | transl_addressing_correctDavid Monniaux2020-03-241-4/+9
| | | | | |
| | | | * | transl_op_correctDavid Monniaux2020-03-241-10/+14
| | | | | |
| | | | * | transl_condDavid Monniaux2020-03-241-143/+332
| | | | | |
| | | | * | progress in proofs about RADavid Monniaux2020-03-242-36/+92
| | | | | |
| | | | * | exec_straight_stepsDavid Monniaux2020-03-241-5/+7
| | | | |/ | | | | | | | | | | | | | | | | | | | | exec_straight_steps_goto exec_straight_opt_steps_goto
| | | | * Include typedef name in error message (#228)Bernhard Schommer2020-03-041-2/+2
| | | | | | | | | | | | | | | In case of redefinition of a typedef name with a different type.
| | | | * Update the RISC-V calling conventions, continued (#227)Xavier Leroy2020-03-021-7/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Double FP arguments passed on stack were incorrectly aligned: they must be 8-aligned but were 4-aligned only. This was due to the use of `Location.typealign`, which is the minimal hardware-supported alignment for a given type, namely 1 word for type Tfloat. To get the correct alignments, `Location.typesize` must be used instead.
| | | * | essai d'avoir le pipeline en manuel OU sur certaines branchesDavid Monniaux2020-03-211-31/+64
| | | | |
| | | * | tentative pour n'avoir le gitlab-ci que sur mppa-work, mppa-k1c et masterDavid Monniaux2020-03-211-0/+31
| | | | |
| | | * | la lib standard ne passe pas en rv32, ne pas la tester en CIDavid Monniaux2020-03-201-1/+1
| | | | |
| | | * | +k1c targetDavid Monniaux2020-03-201-0/+11
| | | | |
| | | * | apt updateDavid Monniaux2020-03-201-7/+10
| | | | |
generated by cgit (git 2.34.1) at 2024-07-13 11:33:37 +0000