aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/SimplLocalsproof.v
Commit message (Expand)AuthorAgeFilesLines
* An improved PTree data structure (#420)Xavier Leroy2021-11-161-1/+0
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-1/+1
* Native support for bit fields (#400)Xavier Leroy2021-08-221-22/+38
* Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-13/+27
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-50/+50
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-1/+1
* Import prim token notations before using themJason Gross2018-08-271-1/+1
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-5/+5
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-30/+42
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-1/+0
* Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-201-53/+46
|\
| * Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-061-53/+46
* | Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-021-104/+5
|/
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-361/+361
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-22/+152
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-18/+18
* Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-3/+0
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-93/+109
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-3/+9
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-3/+7
* Merge of "newspilling" branch:xleroy2014-07-231-32/+25
* Remove useless checks on type_of_global in dynamic semanticsxleroy2014-02-201-12/+1
* Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).xleroy2013-12-301-38/+85
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-2/+2
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-12/+58
* Revised treatment of _Alignas, for better compatibility with GCC and Clang, a...xleroy2013-11-061-7/+11
* Merge of the "alignas" branch.xleroy2013-10-051-8/+10
* Revised handling of int->float conversions:xleroy2013-07-081-1/+4
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-1/+2
* Merge of the "princeton" branch:xleroy2013-06-161-83/+82
* driver: removed option -flonglongxleroy2013-04-221-0/+4
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-196/+48
* Pointers one pastxleroy2013-02-151-18/+27
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-3/+3
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-26/+26
* Avoid generating some obviously useless casts.xleroy2013-01-081-1/+22
* Merge of the clightgen branch:xleroy2012-12-291-0/+2277
generated by cgit (git 2.34.1) at 2024-05-08 13:16:28 +0000