aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-29110-2695/+2694
* Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
* Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-2830-638/+1841
* configure: simplify the final printing of the configurationXavier Leroy2020-12-281-9/+8
* configure: add -mandir option (#382)Daniel Dickman2020-12-281-1/+7
* AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix)Xavier Leroy2020-12-261-1/+1
* AArch64: macOS portXavier Leroy2020-12-2618-220/+570
* C parser: handle other built-in types than __builtin_va_listXavier Leroy2020-12-261-1/+2
* AArch64: clarify the printing of extending-register arithmetic operationsXavier Leroy2020-12-261-13/+13
* AArch64: wrong function alignmentXavier Leroy2020-12-261-1/+1
generated by cgit (git 2.34.1) at 2024-06-29 03:21:47 +0000