aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Ctyping.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-10-041-3/+3
|\
| * Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-031-3/+3
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-9/+45
|\|
| * Native support for bit fields (#400)Xavier Leroy2021-08-221-9/+45
| * 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
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-17/+17
|\|
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-4/+4
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-12/+12
| * Changed cc_varargs to an option typeBernhard Schommer2020-12-251-1/+1
* | Oexpect in frontendDavid Monniaux2020-04-071-0/+3
|/
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-30/+56
* Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-121-0/+1
* Make __builtin_sel available from C source codeXavier Leroy2019-07-171-18/+59
* Regression: handling of integer + pointer in CompCert CXavier Leroy2016-10-061-9/+3
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-68/+109
* Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-201-59/+21
|\
| * Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-061-59/+21
* | Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-021-7/+10
|/
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-119/+119
* In AST.calling_conventions, record whether the original C function was "old-s...Xavier Leroy2015-05-221-10/+12
* Missing case in type_conditional (long long vs. int or float).Xavier Leroy2015-05-221-6/+3
* Ctyping: better typing of conditional expressions.Xavier Leroy2015-05-211-28/+176
* Omission: forgot to treat pointer values in bool_of_val and sem_notbool.Xavier Leroy2015-03-291-2/+3
* Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-1/+0
* Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-0/+1999
* Merge of branches/full-expr-4:xleroy2010-08-181-459/+0
* Support for inlined built-ins.xleroy2010-06-291-6/+12
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-3/+3
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-0/+7
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-4/+4
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-49/+47
* Documentationxleroy2007-08-051-3/+9
* Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure...xleroy2006-09-111-4/+9
* Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)xleroy2006-09-061-4/+9
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-4/+4
* Fusion de la branche "traces":xleroy2006-09-041-0/+420
generated by cgit (git 2.34.1) at 2024-05-08 03:54:02 +0000