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
*
- Extended traces so that pointers within globals are supported as event values.
xleroy
2010-05-10
32
-351
/
+507
*
Another regression
xleroy
2010-05-10
3
-1
/
+10
*
Fewer float axioms.
xleroy
2010-05-09
2
-6
/
+3
*
Suppressed axioms Float.eq_zero_{true,false}, since the latter is
xleroy
2010-05-09
3
-14
/
+8
*
Revised encoding/decoding of floats
xleroy
2010-05-09
8
-231
/
+261
*
Cleaned up handling of linker sections.
xleroy
2010-05-08
9
-229
/
+385
*
Improved coalescing heuristics based on Hailperin's paper.
xleroy
2010-05-08
1
-32
/
+49
*
Cosmetic: comments to mark expansions of some pseudoinstructions.
xleroy
2010-05-08
1
-7
/
+17
*
Update
xleroy
2010-05-05
1
-1
/
+24
*
Strengthen chunktype inference and use it to remove some useless casts.
xleroy
2010-05-05
3
-24
/
+142
*
More theorems about sign and zero extensions
xleroy
2010-05-05
1
-0
/
+100
*
Removed an ADMITTED that was unused, fortunately
xleroy
2010-05-05
1
-2
/
+0
*
Pretty-printers for RTL and LTL. Not yet well integrated.
xleroy
2010-05-02
4
-0
/
+235
*
Compute spill costs.
xleroy
2010-05-02
1
-8
/
+92
*
In compilation of Sassign, avoid systematic move from a fresh temp.
xleroy
2010-05-02
3
-105
/
+211
*
Add "fabs" (floating-point absolute value) as a unary operator in
xleroy
2010-05-02
7
-5
/
+39
*
Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).
xleroy
2010-05-02
2
-0
/
+28
*
ARM version of Machregsaux
xleroy
2010-05-01
2
-0
/
+59
*
More struct tests
xleroy
2010-04-17
1
-1
/
+2
*
__builtin_memcpy, continued.
xleroy
2010-04-17
7
-20
/
+117
*
Support __builtin_memcpy; use it for struct assignment
xleroy
2010-04-17
5
-30
/
+93
*
Update for 1.7.1
v1.7.1
xleroy
2010-04-13
1
-0
/
+17
*
PowerPC:
xleroy
2010-04-10
3
-3
/
+32
*
Coloring: allow to exclude user-specified registers from allocation.
xleroy
2010-04-10
5
-28
/
+131
*
Test bit field of size 32
xleroy
2010-04-09
3
-1
/
+18
*
Bug fix: infinite loop in cparser/ on bit field of size 32 bits.
xleroy
2010-04-09
10
-59
/
+53
*
Static initialization of structs with bitfields
xleroy
2010-04-07
3
-1
/
+109
*
Wrong type for __builtin_volatile_*_int32
xleroy
2010-04-02
1
-1
/
+1
*
In cparser/SimplExpr.ml:
xleroy
2010-04-02
4
-12
/
+30
*
cparser/AddCasts.ml: forgot to materialize cast at return statement.
xleroy
2010-04-01
4
-13
/
+29
*
Updates for release 1.7
v1.7
xleroy
2010-03-30
2
-9
/
+64
*
Update for 1.7
xleroy
2010-03-30
2
-2
/
+8
*
Determine endianness at run-time
xleroy
2010-03-30
1
-21
/
+23
*
Options -I -D -U with a space
xleroy
2010-03-30
1
-0
/
+3
*
Updated Linux conventions
xleroy
2010-03-30
1
-3
/
+6
*
Cleaner generation of .depend
xleroy
2010-03-30
2
-69
/
+65
*
Include targets of preference edges in all_interf_regs. Not needed for corre...
xleroy
2010-03-30
1
-6
/
+8
*
Pretty strings
xleroy
2010-03-29
1
-3
/
+8
*
Extra volatile test
xleroy
2010-03-28
3
-1
/
+45
*
More resistant proof
xleroy
2010-03-28
1
-1
/
+0
*
Prettier printing of configuration
xleroy
2010-03-28
1
-1
/
+2
*
Updated ARM asm printer
xleroy
2010-03-28
1
-4
/
+67
*
Typo
xleroy
2010-03-28
1
-1
/
+0
*
Emit a few comments to help reading the generated asm
xleroy
2010-03-28
1
-10
/
+16
*
Updating ARM port
xleroy
2010-03-28
4
-61
/
+41
*
Bug in multidimensional read-only arrays
xleroy
2010-03-13
2
-7
/
+10
*
TeX and HTML escapes
xleroy
2010-03-12
1
-0
/
+4
*
Copyright notice
xleroy
2010-03-12
1
-0
/
+18
*
Restored the big-step semantics for Cminor
xleroy
2010-03-11
1
-125
/
+125
*
New HTML documentation generator
xleroy
2010-03-09
5
-50
/
+570
[next]