aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
* Use Flocq for floatsxleroy2012-06-281-1/+1
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-4/+12
* Memdata: cleanup continuedxleroy2012-05-261-178/+105
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-264-313/+174
* Merge of the newmem branch:xleroy2012-05-214-1355/+1182
* Hack with nxorxleroy2012-05-181-0/+5
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-282-4/+2
* MAJ docv1.10xleroy2012-03-121-0/+1
* Minor updatesxleroy2012-03-111-2/+2
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-095-105/+782
* Simplified and cleaned up the passing of information from C2C to PrintAsm, as...xleroy2012-02-222-108/+85
* Merge of the "volatile" branch:xleroy2012-02-044-259/+698
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-153-0/+192
* Merge of the nonstrict-ops branch:xleroy2012-01-144-237/+296
* Cleaned up old commented-out partsxleroy2011-08-194-58/+0
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-282-99/+218
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-154-660/+2111
* Back from Oregon commit. xleroy2011-07-055-29/+964
* Forgot to add new filexleroy2011-06-141-0/+40
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-132-63/+153
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-s...xleroy2011-04-162-13/+44
* Merge of branch "unsigned-offsets":xleroy2011-04-094-80/+93
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-6/+6
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-2/+2
* Memory.v: added drop_perm operationxleroy2010-09-213-46/+427
* Merge of the reuse-temps branch:xleroy2010-09-023-2/+45
* Semantics of annotationsxleroy2010-09-021-5/+69
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extxleroy2010-08-211-50/+32
* Merge of branches/full-expr-4:xleroy2010-08-182-137/+423
* Render unto Caesar... (Mention contribution by Dockins and Steward.)xleroy2010-07-081-0/+2
* Support for inlined built-ins.xleroy2010-06-294-83/+84
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-283-291/+517
* More faithful semantics for volatile reads and writes.xleroy2010-05-234-358/+522
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-103-261/+384
* Fewer float axioms.xleroy2010-05-091-2/+1
* Revised encoding/decoding of floatsxleroy2010-05-092-216/+182
* Cleaned up handling of linker sections.xleroy2010-05-082-0/+254
* Copyright noticexleroy2010-03-121-0/+18
* Merge of the newmem and newextcalls branches:xleroy2010-03-079-3869/+6688
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...xleroy2010-03-032-6/+1
* Existence of behaviorsxleroy2010-01-312-15/+176
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-21/+17
* Added support for jump tables in back end.xleroy2009-11-101-12/+131
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-012-0/+5
* No '\n' in Coq strings...xleroy2009-08-181-2/+2
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-163-60/+790
* Added 'going wrong' behaviorsxleroy2009-08-051-11/+34
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-058-107/+107
* Added tail call optimization passxleroy2009-03-262-0/+26
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-261-0/+17
generated by cgit (git 2.34.1) at 2024-06-02 19:37:23 +0000