aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | | | * | Remove `-version-file` option from option summaryXavier Leroy2021-04-231-1/+0
| | | | * | Move `$` notation in submodule `ClightNotations` and scope `clight_scope`Xavier Leroy2021-04-231-11/+23
| | | | * | Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-194-36/+16
| | | | * | Bump minimal Coq version to 8.9.0Xavier Leroy2021-04-191-2/+2
| | | | * | Elab bitfields: check size of type <=32bit rather than checking rank (#387)Amos Robinson2021-04-194-2/+25
| | | | * | Refactor cparser/Parse.mlXavier Leroy2021-04-191-31/+29
| | | | * | Ensure compatibility with future versions of MenhirLibXavier Leroy2021-04-191-6/+7
| | | | * | Do not depend on projection parameter names (#388)Xia Li-yao2021-03-251-1/+1
| | | * | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-0177-1940/+4260
| | | |\ \ \
| | | | * | | removing some Expansion when loading float/single constantsLéo Gourdin2021-06-011-16/+22
| | | | * | | 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
generated by cgit (git 2.34.1) at 2024-06-27 09:27:53 +0000