aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cshmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-1/+1
|\
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-1/+1
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-59/+162
|\|
| * Native support for bit fields (#400)Xavier Leroy2021-08-221-59/+162
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-10/+10
|\|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-10/+10
* | Oexpect in frontendDavid Monniaux2020-04-071-16/+22
|/
* Support re-normalization of values returned by function callsXavier Leroy2020-02-211-29/+104
* Regression: handling of integer + pointer in CompCert CXavier Leroy2016-10-061-56/+40
* Remove usage of do.Bernhard Schommer2016-10-041-58/+58
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-142/+323
* Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-201-217/+343
|\
| * Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-061-217/+343
* | Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-021-15/+25
|/
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-170/+170
* Signedness issue in specification of subtraction between two pointers.Xavier Leroy2015-06-301-2/+13
* Omission: forgot to treat pointer values in bool_of_val and sem_notbool.Xavier Leroy2015-03-291-3/+10
* Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-1/+0
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-74/+80
* Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-261-30/+6
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-3/+7
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-2/+10
* Merge of "newspilling" branch:xleroy2014-07-231-59/+72
* __builtin_absfloat can be applied to integers too.xleroy2014-03-291-1/+12
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-19/+24
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-8/+35
* - Recognize __builtin_fabs as an operator, not just a builtin,xleroy2013-11-061-0/+1
* Revised treatment of _Alignas, for better compatibility with GCC and Clang, a...xleroy2013-11-061-2/+2
* Merge of the "alignas" branch.xleroy2013-10-051-2/+2
* Revised handling of int->float conversions:xleroy2013-07-081-3/+7
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-3/+3
* Merge of the "princeton" branch:xleroy2013-06-161-2/+2
* Revised semantics and compilation of 2-argument C operators to better match xleroy2013-05-061-18/+18
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-2/+7
* driver: removed option -flonglongxleroy2013-04-221-0/+12
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-277/+249
* Pointers one pastxleroy2013-02-151-1/+2
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-5/+5
* Merge of the clightgen branch:xleroy2012-12-291-310/+76
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-29/+8
* Make Clight independent of CompCert C.xleroy2012-10-081-11/+11
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-431/+146
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-4/+2
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-8/+6
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-2/+0
* Merge of the "volatile" branch:xleroy2012-02-041-175/+344
* Merge of the nonstrict-ops branch:xleroy2012-01-141-9/+11
* Cleaned up old commented-out partsxleroy2011-08-191-12/+0
* Improved semantics of castsxleroy2011-07-171-55/+53
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...xleroy2011-07-161-110/+73
generated by cgit (git 2.34.1) at 2024-05-08 21:51:22 +0000