aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Add switch of passinl-cse-constYann Herklotz2021-06-101-12/+12
* 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
* 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
generated by cgit (git 2.34.1) at 2024-05-03 01:35:41 +0000