aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | | * | | Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-0610-197/+268
| | * | | | Adding a flag to test fp_init_expLéo Gourdin2021-03-023-150/+159
| | * | | | Adding fp init expansionsLéo Gourdin2021-03-022-3/+18
| | * | | | Merge remote-tracking branch 'origin/riscv-still-asmcondexp' into riscv-work-...Léo Gourdin2021-03-023-96/+1088
| | |\ \ \ \
| | | * | | | Asmcondexp branche useful to benchmark expansionsLéo Gourdin2021-03-023-96/+1088
| | * | | | | [Admitted checker] Oracle expansion for float/float32 constant initLéo Gourdin2021-03-024-10/+31
| | | |/ / / | | |/| | |
| * / | | | adding test for load replacement on a64Léo Gourdin2021-03-294-0/+61
| |/ / / /
* | | | | 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
generated by cgit (git 2.34.1) at 2024-07-11 23:12:21 +0000