aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* 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
* "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
generated by cgit (git 2.34.1) at 2024-05-20 08:27:26 +0000