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
/
Asm.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Tentative first fix for offsets of ld/std.
Bernhard Schommer
2021-04-24
1
-0
/
+2
*
Replace `omega` tactic with `lia`
Xavier Leroy
2020-12-29
1
-1
/
+1
*
PowerPC modeling of registers destroyed by pseudo-instructions
Xavier Leroy
2020-12-06
1
-1
/
+1
*
Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions
Xavier Leroy
2020-12-06
1
-9
/
+0
*
Model GPR0 in isel (#199)
Xavier Leroy
2019-09-17
1
-1
/
+1
*
Provide a float select operation for PowerPC. (#173)
Bernhard Schommer
2019-05-28
1
-0
/
+8
*
Emulate the "isel" instruction on non-EREF PPC processors
Xavier Leroy
2019-05-20
1
-1
/
+1
*
Give a semantics to the Pisel instruction
Xavier Leroy
2019-05-20
1
-1
/
+7
*
Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776
Michael Schmidt
2018-10-20
1
-2
/
+2
*
Model external calls as destroying all caller-save registers
Xavier Leroy
2018-06-01
1
-1
/
+10
*
Add new powerpc builtins.
Michael Schmidt
2018-04-27
1
-0
/
+4
*
Hybrid 64bit/32bit PowerPC port
Bernhard Schommer
2017-05-03
1
-10
/
+167
*
Give explicit scopes to notations a#b and a##b and a#b<-c
Xavier Leroy
2017-02-13
1
-4
/
+6
*
Support for 64-bit architectures: update the PowerPC port
Xavier Leroy
2016-10-01
1
-29
/
+29
*
Introduce register pairs to describe calling conventions more precisely
Xavier Leroy
2016-05-17
1
-17
/
+34
*
Bug 17752, add rldicr instruction for PowerPC
Michael Schmidt
2015-12-15
1
-1
/
+3
*
bug 17392: remove trailing whitespace in source files
Michael Schmidt
2015-10-14
1
-9
/
+9
*
Use PowerPC 64 bits instructions (when available) for int<->FP conversions.
Xavier Leroy
2015-09-13
1
-0
/
+19
*
Added builtin for isel.
Bernhard Schommer
2015-09-08
1
-0
/
+2
*
Added builtins for call frame and return address.
Bernhard Schommer
2015-09-07
1
-3
/
+3
*
Added builtin for the cmpb instruction.
Bernhard Schommer
2015-09-07
1
-0
/
+2
*
Added builtin for mbar instruction.
Bernhard Schommer
2015-09-03
1
-0
/
+2
*
New builtin for dcbz instruction.
Bernhard Schommer
2015-09-03
1
-8
/
+10
*
Added builtin for the icbtls instruction.
Bernhard Schommer
2015-09-02
1
-0
/
+2
*
Added builtin for dcbtls
Bernhard Schommer
2015-09-02
1
-1
/
+3
*
Added the gcc builtin prefetch.
Bernhard Schommer
2015-09-01
1
-0
/
+4
*
Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.
Xavier Leroy
2015-08-22
1
-1
/
+1
*
Adapt the PowerPC port to the new builtin representation.
Xavier Leroy
2015-08-21
1
-26
/
+23
*
Added builtin for the dcbf instruction
Bernhard Schommer
2015-08-17
1
-0
/
+2
*
Added builtin for the dcbi instruction.
Bernhard Schommer
2015-08-17
1
-4
/
+4
*
Added builitin for the icbi instruction.
Bernhard Schommer
2015-08-14
1
-0
/
+2
*
Added builtin for the lwsync barrier.
Bernhard Schommer
2015-08-14
1
-0
/
+2
*
Corrected little typo in __builtin_clz function.
Bernhard Schommer
2015-07-06
1
-2
/
+2
*
Changed a minor typo: Pstwxu should be Pstwux
Bernhard Schommer
2015-06-22
1
-2
/
+2
*
Updating the PowerPC and ARM ports.
Xavier Leroy
2015-03-27
1
-35
/
+7
*
Add builtins for load with reservation and conditional store.
xleroy
2014-08-20
1
-0
/
+4
*
powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.
xleroy
2014-08-18
1
-18
/
+8
*
PowerPC port: refactored the expansion of built-in functions and
xleroy
2014-07-28
1
-14
/
+85
*
Merge of "newspilling" branch:
xleroy
2014-07-23
1
-9
/
+51
*
Refactoring: move symbol_offset into Genv.
xleroy
2014-05-24
1
-16
/
+10
*
- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.
xleroy
2014-01-12
1
-4
/
+4
*
Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...
xleroy
2013-12-26
1
-27
/
+26
*
powerpc/: new unary operation "addsymbol"
xleroy
2013-11-17
1
-1
/
+9
*
Optimize integer divisions by positive constants, turning them into
xleroy
2013-07-29
1
-0
/
+6
*
Merge of the "princeton" branch:
xleroy
2013-06-16
1
-1
/
+1
*
Refactoring: move definition of chunk_of_type to AST.v.
xleroy
2013-05-06
1
-3
/
+0
*
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
xleroy
2013-04-20
1
-41
/
+38
*
Revised Stacking and Asmgen passes and Mach semantics:
xleroy
2013-03-01
1
-124
/
+139
*
- Revised non-overflow constraints on memory injections so that
xleroy
2012-07-23
1
-5
/
+5
*
PowerPC: remove the fmadd and fmsub operators/Asm instructions
xleroy
2012-03-07
1
-6
/
+0
[next]