aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * | | Merge branch 'riscv-work-fpinit-stillexp' into kvx-workLéo Gourdin2021-05-190-0/+0
| | |\ \ \
| | | * | | xorimmsubmission_OOPSLA2021_RISCVLéo Gourdin2021-04-092-0/+77
| | | * | | removing useless flag checkLéo Gourdin2021-04-091-3/+1
| | * | | | debug prints uniformizedLéo Gourdin2021-05-181-69/+66
| * | | | | 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
generated by cgit (git 2.34.1) at 2024-07-06 15:49:10 +0000