aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * | Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-245-152/+259
| | * | Update the output of clightgen to pick the `$` notation from its new placeXavier Leroy2021-04-231-1/+3
| | * | 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
| | |/ / /
| | * | | Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-198-48/+1410
| | * | | 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
generated by cgit (git 2.34.1) at 2024-07-01 06:00:42 +0000