aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | | | * | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...Léo Gourdin2021-05-311-1/+0
| | | | |\ \ \
| | | | | * | | just remove a debug printLéo Gourdin2021-05-291-1/+0
| | | | * | | | bugfix A64 peephole (cf Scade/Fighter example)Léo Gourdin2021-05-311-6/+5
| | | | |/ / /
| | | * | | | Commenting out __builtin_expect from AbsIntCyril SIX2021-06-011-2/+2
| | | * | | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-01167-1119/+1692
| | | * | | | Updating varargs2 results for kvxCyril SIX2021-06-011-0/+1
| | | * | | | Remove /home/yuki/Work/VERIMAG/CompCertCyril SIX2021-06-011-1/+1
| | | * | | | fix aarch64 merge?Léo Gourdin2021-03-297-846/+19
| | | * | | | replacing omega with lia in some fileLéo Gourdin2021-03-2933-267/+296
| | | * | | | fix riscv merge?Léo Gourdin2021-03-295-488/+0
| | | * | | | fix CI arm and armhfSylvain Boulmé2021-03-241-2/+6
| | | * | | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-23201-4415/+9534
| | | |\ \ \ \ | | | | | |/ / | | | | |/| |
| | | | * | | Coq 8.13.1 is supportedXavier Leroy2021-03-091-2/+2
| | | | * | | Fix regression on PowerPC / DiabXavier Leroy2021-02-232-4/+11
| | | | * | | Section handling: finer control of variable initializationXavier Leroy2021-02-239-42/+90
| | | | * | | Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-236-35/+34
| | | | * | | Silence some new warnings of Coq 8.13Xavier Leroy2021-01-211-1/+17
| | | | * | | Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-2130-133/+136
| | | | * | | Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
| | | | * | | "macosx" is now called "macos"Xavier Leroy2021-01-1816-25/+25
| | | | * | | macOS: turn #warning offXavier Leroy2021-01-181-2/+2
| | | | * | | Remove regression/interop1 testXavier Leroy2021-01-184-417/+1
| | | | * | | Testing calling conventions and interoperability with another C compilerXavier Leroy2021-01-185-1/+583
| | | | * | | Support re-normalization of function parameters at function entryXavier Leroy2021-01-167-27/+58
| | | | * | | Change warning for pragmas inside functionsXavier Leroy2021-01-161-1/+1
| | | | * | | PowerPC: wrong computation of the position of the first vararg argumentXavier Leroy2021-01-151-2/+3
| | | | * | | Coq 8.13.0 is supportedXavier Leroy2021-01-141-3/+3
| | | | * | | RISC-V: fix FP calling conventionsXavier Leroy2021-01-146-122/+176
| | | | * | | Replace `omega` tactic with `lia`, continuedXavier Leroy2021-01-131-1/+1
| | | | * | | Improve branch tunnelingXavier Leroy2021-01-132-60/+328
| | | | * | | Revised correctness proof for record_gotoXavier Leroy2021-01-131-68/+29
| | | | * | | Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| | | | * | | Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
| | | | * | | RISC-V: wrong fixup code generated for vararg calls with fixed FP argsXavier Leroy2021-01-103-12/+35
| | | | * | | Ignore and warn about pragmas inside functionsXavier Leroy2021-01-071-1/+4
| | | | * | | Replace `omega` tactic with `lia`Xavier Leroy2020-12-29110-2695/+2694
| | | | * | | Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
| | | | * | | Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-2830-638/+1841
| | | | * | | configure: simplify the final printing of the configurationXavier Leroy2020-12-281-9/+8
| | | | * | | configure: add -mandir option (#382)Daniel Dickman2020-12-281-1/+7
| | | | * | | AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix)Xavier Leroy2020-12-261-1/+1
| | | | * | | AArch64: macOS portXavier Leroy2020-12-2618-220/+570
| | | | * | | C parser: handle other built-in types than __builtin_va_listXavier Leroy2020-12-261-1/+2
| | | | * | | AArch64: clarify the printing of extending-register arithmetic operationsXavier Leroy2020-12-261-13/+13
| | | | * | | AArch64: wrong function alignmentXavier Leroy2020-12-261-1/+1
| | | | * | | RISC-V: revised calling conventions for variadic functionsXavier Leroy2020-12-252-63/+105
| | | | * | | Changed cc_varargs to an option typeBernhard Schommer2020-12-2512-27/+36
| | | | * | | configure: use `$make` instead of `make`Xavier Leroy2020-12-251-1/+1
| | | | * | | configure script revised and simplifiedXavier Leroy2020-12-241-83/+43
| | | | * | | configure: support Coq 8.12.2Xavier Leroy2020-12-241-2/+2
generated by cgit (git 2.34.1) at 2024-07-11 23:31:11 +0000