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
path:
root
/
powerpc
/
Machregs.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...
Xavier Leroy
2016-04-27
1
-1
/
+30
*
bug 17752, add constant propagation for builtins
Michael Schmidt
2015-12-15
1
-1
/
+3
*
bug 17752, add builtin64_set_spr and builtin64_get_spr for PowerPC
Michael Schmidt
2015-12-15
1
-1
/
+2
*
bug 17752, add builtin_mr for PowerPC
Michael Schmidt
2015-12-14
1
-3
/
+4
*
Merge remote-tracking branch 'origin/master' into named-externals
Bernhard Schommer
2015-10-20
1
-1
/
+1
|
\
|
*
bug 17392: remove trailing whitespace in source files
Michael Schmidt
2015-10-14
1
-1
/
+1
|
*
Merge branch 'master' into ppc64
Xavier Leroy
2015-10-11
1
-2
/
+17
|
|
\
|
*
|
Use PowerPC 64 bits instructions (when available) for int<->FP conversions.
Xavier Leroy
2015-09-13
1
-1
/
+1
*
|
|
Updated PR by removing whitespaces. Bug 17450.
Bernhard Schommer
2015-10-20
1
-1
/
+1
*
|
|
Use Coq strings instead of idents to name external and builtin functions.
Xavier Leroy
2015-10-11
1
-22
/
+11
|
|
/
|
/
|
*
|
Applied a few simplification for temporary registers.
Bernhard Schommer
2015-09-21
1
-3
/
+2
*
|
Use fix registers for atomic builtins.
Bernhard Schommer
2015-09-14
1
-5
/
+12
*
|
Added builtin for atomic compare and exchange.
Bernhard Schommer
2015-09-10
1
-0
/
+2
*
|
Merge branch 'master' into atomic-builtins
Bernhard Schommer
2015-09-10
1
-2
/
+3
|
\
|
*
|
Added an builtin for the atomic exchange operation.
Bernhard Schommer
2015-09-09
1
-1
/
+7
|
/
*
Simplified generation of builtins for cache instructions.
Bernhard Schommer
2015-09-07
1
-3
/
+3
*
Added builtin for mbar instruction.
Bernhard Schommer
2015-09-03
1
-0
/
+2
*
Added builtin for the icbtls instruction.
Bernhard Schommer
2015-09-02
1
-0
/
+2
*
Added builtin for dcbtls
Bernhard Schommer
2015-09-02
1
-0
/
+2
*
Added the gcc builtin prefetch.
Bernhard Schommer
2015-09-01
1
-0
/
+2
*
Adapt the PowerPC port to the new builtin representation.
Xavier Leroy
2015-08-21
1
-5
/
+23
*
Extended inline asm: revised treatment of clobbered registers.
Xavier Leroy
2015-05-09
1
-0
/
+42
*
Merge of "newspilling" branch:
xleroy
2014-07-23
1
-27
/
+10
*
In Regalloc, dead code elimination, don't eliminate move operations
xleroy
2014-02-23
1
-0
/
+2
*
Merge of the float32 branch:
xleroy
2013-05-19
1
-1
/
+7
*
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
xleroy
2013-04-20
1
-31
/
+93
*
Merge of the reuse-temps branch:
xleroy
2010-09-02
1
-12
/
+15
*
Adapted to work with Coq 8.2-1
v1.4.1
xleroy
2009-06-05
1
-1
/
+1
*
Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...
xleroy
2009-02-26
1
-9
/
+9
*
Reorganized the development, modularizing away machine-dependent parts.
xleroy
2008-12-30
1
-0
/
+107