aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Csem.v
Commit message (Expand)AuthorAgeFilesLines
* Native support for bit fields (#400)Xavier Leroy2021-08-221-46/+60
* 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-4/+4
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-1/+1
* Make __builtin_sel available from C source codeXavier Leroy2019-07-171-13/+56
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-15/+15
* Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-021-20/+17
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-9/+9
* Omission: forgot to treat pointer values in bool_of_val and sem_notbool.Xavier Leroy2015-03-291-13/+13
* Interpreter produces more detailed trace, including name of semantic rules used.Xavier Leroy2015-02-081-1/+1
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-44/+52
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-131-8/+8
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-5/+6
* Use "incrdecr_type ty" instead of "typeconv ty" as the intermediate typexleroy2014-04-151-1/+3
* Remove useless checks on type_of_global in dynamic semanticsxleroy2014-02-201-14/+0
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-6/+6
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-8/+21
* Merge of the "alignas" branch.xleroy2013-10-051-1/+2
* Merge of the clightgen branch:xleroy2012-12-291-1/+0
* Make Clight independent of CompCert C.xleroy2012-10-081-519/+2
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-39/+95
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-2/+6
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-0/+3
* Merge of the "volatile" branch:xleroy2012-02-041-91/+180
* Cleaned up old commented-out partsxleroy2011-08-191-34/+0
* Improved semantics of castsxleroy2011-07-171-0/+39
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...xleroy2011-07-161-127/+96
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-6/+3
* Fix treatment of function pointers at function calls in the CompCert C and Cl...xleroy2011-07-141-2/+3
* Merge of branch "unsigned-offsets":xleroy2011-04-091-6/+11
* Initializers for global variables: compile-time evaluation of expressions don...xleroy2011-03-121-1/+1
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-3/+4
* Nettoyages pour docxleroy2010-08-181-2/+2
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-181-2/+0
* Merge of branches/full-expr-4:xleroy2010-08-181-1176/+617
* Support for inlined built-ins.xleroy2010-06-291-6/+6
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-2/+2
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-2/+2
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isxleroy2010-05-091-3/+4
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-021-0/+7
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-39/+46
* Function types didn't always degrade to pointers like they should. Introduce...xleroy2010-03-021-1/+1
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-3/+3
* Last updates for release 1.5.v1.5xleroy2009-08-281-9/+9
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-25/+31
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-99/+876
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-1/+1
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-4/+4
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-5/+10
* Utilisation de intoffloatu. Ajout du cas int + ptr.xleroy2008-05-311-10/+22
generated by cgit (git 2.34.1) at 2024-05-08 20:56:01 +0000