index
:
debian-compcert
master
pristine-tar
upstream
Debian packaging for CompCert
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Merge of the reuse-temps branch:
xleroy
2010-09-02
*
Semantics of annotations
xleroy
2010-09-02
*
Adding __builtin_annotation
xleroy
2010-09-01
*
Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of readi...
xleroy
2010-09-01
*
Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext
xleroy
2010-08-21
*
Nettoyages pour doc
xleroy
2010-08-18
*
Removed useless constraints on return type at Sreturn instructions
xleroy
2010-08-18
*
Copyright banner
xleroy
2010-08-18
*
Renamed C2Clight into C2C
xleroy
2010-08-18
*
Merge of branches/full-expr-4:
xleroy
2010-08-18
*
Wrong cast in constant_expr
xleroy
2010-08-04
*
Fix extraction problem
xleroy
2010-07-14
*
Preliminary support for gcc-style __attribute__ over types
xleroy
2010-07-08
*
Bug in cparser/AddCasts.ml.
xleroy
2010-07-08
*
Render unto Caesar... (Mention contribution by Dockins and Steward.)
xleroy
2010-07-08
*
Forgot to add this file. Part of the refactoring of $ARCH/$SYSTEM/Conventions.v
xleroy
2010-07-07
*
Support for inlined built-ins.
xleroy
2010-06-29
*
All axioms used in the CompCert development
xleroy
2010-06-28
*
Merging the Princeton implementation of the memory model. Separate axioms in...
xleroy
2010-06-28
*
Updated Caml parts to match new representation for global variables.
xleroy
2010-05-26
*
Clean up
xleroy
2010-05-26
*
Typo in documentation
xleroy
2010-05-26
*
More faithful semantics for volatile reads and writes.
xleroy
2010-05-23
*
- Extended traces so that pointers within globals are supported as event values.
xleroy
2010-05-10
*
Another regression
xleroy
2010-05-10
*
Fewer float axioms.
xleroy
2010-05-09
*
Suppressed axioms Float.eq_zero_{true,false}, since the latter is
xleroy
2010-05-09
*
Revised encoding/decoding of floats
xleroy
2010-05-09
*
Cleaned up handling of linker sections.
xleroy
2010-05-08
*
Improved coalescing heuristics based on Hailperin's paper.
xleroy
2010-05-08
*
Cosmetic: comments to mark expansions of some pseudoinstructions.
xleroy
2010-05-08
*
Update
xleroy
2010-05-05
*
Strengthen chunktype inference and use it to remove some useless casts.
xleroy
2010-05-05
*
More theorems about sign and zero extensions
xleroy
2010-05-05
*
Removed an ADMITTED that was unused, fortunately
xleroy
2010-05-05
*
Pretty-printers for RTL and LTL. Not yet well integrated.
xleroy
2010-05-02
*
Compute spill costs.
xleroy
2010-05-02
*
In compilation of Sassign, avoid systematic move from a fresh temp.
xleroy
2010-05-02
*
Add "fabs" (floating-point absolute value) as a unary operator in
xleroy
2010-05-02
*
Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).
xleroy
2010-05-02
*
ARM version of Machregsaux
xleroy
2010-05-01
*
More struct tests
xleroy
2010-04-17
*
__builtin_memcpy, continued.
xleroy
2010-04-17
*
Support __builtin_memcpy; use it for struct assignment
xleroy
2010-04-17
*
Update for 1.7.1
xleroy
2010-04-13
*
PowerPC:
xleroy
2010-04-10
*
Coloring: allow to exclude user-specified registers from allocation.
xleroy
2010-04-10
*
Test bit field of size 32
xleroy
2010-04-09
*
Bug fix: infinite loop in cparser/ on bit field of size 32 bits.
xleroy
2010-04-09
*
Static initialization of structs with bitfields
xleroy
2010-04-07
[next]