aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Replace omega by liaYann Herklotz2021-09-177-52/+57
* Merge remote-tracking branch 'upstream/master'Yann Herklotz2021-09-17328-8336/+12753
|\
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-158-5/+13
| * clightgen: handle empty names given to padding bit fieldsXavier Leroy2021-09-152-16/+28
| * Handle the new warnings of OCaml 4.13Xavier Leroy2021-09-132-4/+4
| * Share code for memory access for PowerPCBernhard Schommer2021-09-064-166/+159
| * Protect against overflows in `leaq` (all forms)Bernhard Schommer2021-08-271-22/+27
| * Protect against overflows in `leaq N(src), dst` (#407)Xavier Leroy2021-08-271-12/+17
| * Merge branch 'bitfields' (#400)Xavier Leroy2021-08-2245-2305/+4004
| |\
| | * Native support for bit fields (#400)Xavier Leroy2021-08-2242-2299/+3866
| | * Add Ctypes.link_match_program_genXavier Leroy2021-08-221-0/+52
| | * Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-223-6/+6
| | * Add `floor` and some propertiesXavier Leroy2021-07-261-0/+37
| | * More lemmas about `align`Xavier Leroy2021-07-261-0/+17
| | * More lemmas about list appendXavier Leroy2021-07-261-0/+26
| * | Revise the declaration of __compcert_* helper functionsXavier Leroy2021-06-301-82/+79
| * | x86 assembly: fix the comment delimiter for macos and make it per-OSXavier Leroy2021-06-101-3/+11
| * | Support `# 0 ...` preprocessed line directiveXavier Leroy2021-06-011-1/+1
| |/
| * Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-132-3/+5
| * Update for release 3.9v3.9Xavier Leroy2021-05-101-1/+1
| * Update Changelog for release 3.9Xavier Leroy2021-05-091-0/+3
| * Update for release 3.9Xavier Leroy2021-05-091-4/+5
| * Update ChangelogXavier Leroy2021-05-081-1/+11
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-08149-860/+1171
| * Fix evaluation order in emulation of bitfield assignmentXavier Leroy2021-05-021-2/+2
| * Support __builtin_expectXavier Leroy2021-05-021-0/+5
| * Support __builtin_unreachableXavier Leroy2021-05-028-2/+32
| * Fix spurious error on initialization of struct with flexible array memberXavier Leroy2021-05-021-0/+3
| * Update ChangelogXavier Leroy2021-04-291-0/+53
| * Emit no entry for variables without init in json.Bernhard Schommer2021-04-291-1/+7
| * MacOS: add a #define __DARWIN_OS_INLINEXavier Leroy2021-04-271-2/+2
| * Support Coq 8.13.2Xavier Leroy2021-04-271-2/+2
| * More fixes for ld/std issue.Bernhard Schommer2021-04-241-11/+40
| * 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
| * 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
generated by cgit (git 2.34.1) at 2024-06-29 10:38:09 +0000