aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Ctypes.v
Commit message (Expand)AuthorAgeFilesLines
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-4/+4
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-0/+2
* Native support for bit fields (#400)Xavier Leroy2021-08-221-124/+461
* Add Ctypes.link_match_program_genXavier Leroy2021-08-221-0/+52
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-19/+22
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-0/+1
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-3/+16
* Use `Program Instance` instead of `Instance` + refine mode (#261)Maxime Dénès2018-12-271-23/+33
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-28/+28
* An hypothesis has changed name.Maxime Dénès2017-01-091-1/+1
* The subst tactic has become more powerful.Maxime Dénès2017-01-091-1/+1
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-22/+28
* Define linking for Csyntax and Clight programs.Xavier Leroy2016-03-061-23/+506
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-58/+58
* Ctypes.composite_of_def: make sure it computes within Coq.Xavier Leroy2015-09-181-3/+3
* Define a nonnegative integer "rank" for types to support structural induction...Xavier Leroy2015-01-101-18/+116
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-331/+552
* Merge of "newspilling" branch:xleroy2014-07-231-9/+12
* Clean-up pass on C types:xleroy2014-04-231-4/+41
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-7/+12
* Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).xleroy2013-12-301-18/+15
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-13/+23
* Revised treatment of _Alignas, for better compatibility with GCC and Clang, a...xleroy2013-11-061-52/+121
* Merge of the "alignas" branch.xleroy2013-10-051-85/+146
* Merge of the float32 branch: xleroy2013-05-191-0/+2
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-3/+10
* Make Clight independent of CompCert C.xleroy2012-10-081-0/+546
generated by cgit (git 2.34.1) at 2024-05-08 22:28:33 +0000