index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
Revised handling of sizeof(string-literal)
xleroy
2011-03-15
6
-7
/
+41
*
Special case for while(1), for(..., 1, ...) and do ... while(0) loops.
xleroy
2011-03-15
2
-22
/
+69
*
Update for 1.8.1
xleroy
2011-03-14
1
-2
/
+2
*
Update for 1.8.1 release
v1.8.1
xleroy
2011-03-14
2
-5
/
+31
*
Incompatibility 8.3 / 8.3pl1
xleroy
2011-03-14
1
-1
/
+1
*
Comment char for Diab
xleroy
2011-03-13
1
-1
/
+1
*
Slightly nicer semantics for initialization
xleroy
2011-03-13
1
-28
/
+29
*
More global initialization work done and proved in Coq.
xleroy
2011-03-13
4
-80
/
+410
*
Initializers for global variables: compile-time evaluation of expressions don...
xleroy
2011-03-12
11
-159
/
+891
*
Undesirable optimization of 'print'
xleroy
2011-03-10
1
-0
/
+2
*
Bitfields: MSB-to-LSB in addition to LSB-to-MSB
xleroy
2011-03-10
3
-11
/
+39
*
Revised signed/unsigned char handling.
xleroy
2011-03-10
4
-18
/
+8
*
Improved test harness
xleroy
2011-03-10
3
-0
/
+14
*
Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.
xleroy
2011-03-09
18
-85
/
+70
*
Treat "char" as unsigned OR signed depending on the configuration.
xleroy
2011-03-09
8
-10
/
+58
*
Use movapd instead of movsd for xmm reg-reg move: it avoids partial register ...
xleroy
2010-11-28
1
-1
/
+1
*
In StructAssign: be careful not to duplicate accesses to a volatile variable.
xleroy
2010-11-10
3
-9
/
+24
*
float->int conversions, continued: weaker axiomatization.
xleroy
2010-10-29
5
-29
/
+9
*
Float.intoffloat and Float.intuoffloat are now partial functions.
xleroy
2010-10-28
21
-62
/
+139
*
Various algorithmic improvements that reduce compile times (thanks Alexandre ...
xleroy
2010-10-27
19
-141
/
+965
*
License for Floataux.ml
xleroy
2010-10-27
2
-1
/
+4
*
Inconsistent treatment of "lone" zero-width bit fields
xleroy
2010-09-24
5
-24
/
+53
*
Bizarre use of struct value
v1.8
xleroy
2010-09-21
2
-2
/
+2
*
Update for release 1.8
xleroy
2010-09-21
3
-18
/
+42
*
Typo in doc comment
xleroy
2010-09-21
1
-2
/
+2
*
Memory.v: added drop_perm operation
xleroy
2010-09-21
3
-46
/
+427
*
No crash if nonexistent input file.
xleroy
2010-09-14
2
-2
/
+3
*
Comments
xleroy
2010-09-10
1
-8
/
+10
*
Improvements for int8 and int16 stores
xleroy
2010-09-10
4
-11
/
+53
*
Updates for IA32-Cygwin.
xleroy
2010-09-08
5
-33
/
+63
*
Updated
xleroy
2010-09-04
2
-12
/
+43
*
++ on volatile not supported.
xleroy
2010-09-04
1
-2
/
+2
*
Update: adding __builtin_annotation
xleroy
2010-09-04
1
-1
/
+36
*
Simplified stdlib wrapper; use it only under MacOS X
xleroy
2010-09-04
7
-278
/
+76
*
Support for __builtin_fmax and __builtin_fmin
xleroy
2010-09-04
2
-1
/
+22
*
Better emulation of long long as a struct.
xleroy
2010-09-04
2
-16
/
+51
*
Merge of the reuse-temps branch:
xleroy
2010-09-02
89
-2579
/
+12842
*
Semantics of annotations
xleroy
2010-09-02
1
-5
/
+69
*
Adding __builtin_annotation
xleroy
2010-09-01
8
-12
/
+219
*
Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of readi...
xleroy
2010-09-01
10
-15
/
+119
*
Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext
xleroy
2010-08-21
7
-1121
/
+1148
*
Nettoyages pour doc
xleroy
2010-08-18
4
-21
/
+15
*
Removed useless constraints on return type at Sreturn instructions
xleroy
2010-08-18
8
-36
/
+28
*
Copyright banner
xleroy
2010-08-18
1
-0
/
+12
*
Renamed C2Clight into C2C
xleroy
2010-08-18
4
-7
/
+7
*
Merge of branches/full-expr-4:
xleroy
2010-08-18
56
-6180
/
+13619
*
Wrong cast in constant_expr
xleroy
2010-08-04
1
-3
/
+3
*
Fix extraction problem
xleroy
2010-07-14
2
-4
/
+4
*
Preliminary support for gcc-style __attribute__ over types
xleroy
2010-07-08
6
-135
/
+168
*
Bug in cparser/AddCasts.ml.
xleroy
2010-07-08
4
-4
/
+22
[prev]
[next]