aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into dev/michalisdev/michalisYann Herklotz2021-09-17337-8490/+12887
|\
| * Fix compilation of verilog back endYann Herklotz2021-09-172-102/+77
| * 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
generated by cgit (git 2.34.1) at 2024-05-02 15:04:22 +0000