aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cop.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-0/+54
|\
| * Native support for bit fields (#400)Xavier Leroy2021-08-221-0/+54
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* | Oexpect in frontendDavid Monniaux2020-04-071-0/+13
|/
* Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-121-2/+2
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-2/+2
* Make __builtin_sel available from C source codeXavier Leroy2019-07-171-0/+21
* Regression: handling of integer + pointer in CompCert CXavier Leroy2016-10-061-32/+46
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-278/+327
* Merge pull request #90 from AbsInt/sem-castsXavier Leroy2016-03-111-50/+176
|\
| * Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-021-50/+176
* | Relaxing the semantics of pointer arithmetic.Xavier Leroy2016-02-291-6/+21
|/
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-54/+54
* Signedness issue in specification of subtraction between two pointers.Xavier Leroy2015-06-301-3/+5
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-26/+26
* Omission: forgot to treat pointer values in bool_of_val and sem_notbool.Xavier Leroy2015-03-291-18/+50
* 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-42/+40
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-1/+25
* Merge of "newspilling" branch:xleroy2014-07-231-74/+200
* Clean-up pass on C types:xleroy2014-04-231-59/+260
* Use "incrdecr_type ty" instead of "typeconv ty" as the intermediate typexleroy2014-04-151-0/+9
* __builtin_absfloat can be applied to integers too.xleroy2014-03-291-17/+36
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-8/+8
* - Recognize __builtin_fabs as an operator, not just a builtin,xleroy2013-11-061-1/+11
* Revised handling of int->float conversions:xleroy2013-07-081-5/+7
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-5/+7
* Merge of the "princeton" branch:xleroy2013-06-161-3/+3
* Revised semantics and compilation of 2-argument C operators to better match xleroy2013-05-061-93/+67
* driver: removed option -flonglongxleroy2013-04-221-25/+34
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-310/+643
* Pointers one pastxleroy2013-02-151-14/+15
* Make Clight independent of CompCert C.xleroy2012-10-081-0/+822
generated by cgit (git 2.34.1) at 2024-05-08 21:13:50 +0000