index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
aarch64
Commit message (
Expand
)
Author
Age
Files
Lines
*
fix new register erasing scheme for AArch64
David Monniaux
2020-12-08
3
-553
/
+241
*
Merge github.com:AbsInt/CompCert into kvx-work
v3.8_kvx_instructions_fixed
David Monniaux
2020-12-08
2
-8
/
+11
|
\
|
*
AArch64 modeling of registers destroyed by pseudo-instructions
Xavier Leroy
2020-12-06
2
-8
/
+11
*
|
Merge branch 'kvx-work' into kvx-work-merge3.8
Cyril SIX
2020-12-04
11
-175
/
+1231
|
\
\
|
*
\
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-11-24
2
-4
/
+76
|
|
\
\
|
|
*
|
fix wrong version of file on AArch64
David Monniaux
2020-11-23
1
-1
/
+4
|
|
*
|
fix bug #223 on AArch64
David Monniaux
2020-11-23
1
-3
/
+72
|
*
|
|
disable debug printing in scheduler
David Monniaux
2020-11-04
1
-3
/
+5
|
*
|
|
new OpWeights for aarch64
David Monniaux
2020-10-22
1
-318
/
+342
|
*
|
|
allow changing target cpu
David Monniaux
2020-10-22
2
-21
/
+40
|
*
|
|
prefix all calls to OpWeights as preparation to using a structure
David Monniaux
2020-10-22
1
-14
/
+14
|
*
|
|
op_valid_pointer_eq for aarch64
David Monniaux
2020-10-19
1
-0
/
+14
|
*
|
|
so that all architectures compile
David Monniaux
2020-10-02
1
-0
/
+473
|
*
|
|
non trapping op
David Monniaux
2020-09-30
4
-88
/
+73
|
*
|
|
non trapping
David Monniaux
2020-09-30
1
-2
/
+0
|
*
|
|
AArch64 division no longer "traps"
David Monniaux
2020-09-30
6
-81
/
+221
|
*
|
|
floating-point division uses the divisor
David Monniaux
2020-09-29
1
-4
/
+5
|
*
|
|
attempt at separating the divisions
David Monniaux
2020-09-29
1
-0
/
+5
|
*
|
|
try to model resources
David Monniaux
2020-09-29
1
-5
/
+164
|
*
|
|
attempt at latencies for Cortex A53
David Monniaux
2020-09-29
1
-2
/
+147
|
*
|
|
first opweights, bogus weights
David Monniaux
2020-09-16
1
-0
/
+19
|
|
/
/
*
|
|
Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8
David Monniaux
2020-11-18
7
-33
/
+34
|
\
\
\
|
|
/
/
|
/
|
/
|
|
/
|
*
Added implementation for fmin/fmax for aarch64.
Bernhard Schommer
2020-11-06
3
-0
/
+12
|
*
Support the use of already-installed MenhirLib and Flocq libraries
Xavier Leroy
2020-09-21
1
-2
/
+1
|
*
Add __builtin_sqrt as synonymous for __builtin_fsqrt
Xavier Leroy
2020-07-27
1
-1
/
+1
|
*
Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml
Xavier Leroy
2020-07-27
1
-8
/
+0
|
*
AArch64 implementation of __builtin_ctz*
Xavier Leroy
2020-07-27
3
-1
/
+11
|
*
No need to process __builtin_fabs in $ARCH/Asmexpand.ml
Xavier Leroy
2020-07-27
1
-2
/
+0
|
*
Move shared code in new file.
Bernhard Schommer
2020-06-28
1
-17
/
+0
|
*
Remove the `can_reserve_register` function.
Bernhard Schommer
2020-06-28
1
-2
/
+0
|
*
Use Hashtbl.find_opt.
Bernhard Schommer
2020-06-28
1
-1
/
+1
|
*
Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}
Xavier Leroy
2020-05-05
3
-0
/
+9
*
|
make Aarch64 muladd depend on the option
David Monniaux
2020-05-06
2
-4
/
+10
*
|
Adding copyrights
Cyril SIX
2020-05-04
3
-0
/
+38
*
|
Merge remote-tracking branch 'origin/mppa-licm' into mppa-features
David Monniaux
2020-04-20
2
-3
/
+10
|
\
\
|
*
|
test whether the instructions are allowed
David Monniaux
2020-04-19
1
-0
/
+2
|
*
|
adapting new stuff for ARM and AArch64
David Monniaux
2020-04-01
1
-3
/
+8
*
|
|
Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features
David Monniaux
2020-04-12
3
-1
/
+43
|
\
\
\
|
*
|
|
fix for aarch64
David Monniaux
2020-04-11
1
-1
/
+1
|
*
|
|
fix writing profiling info for Aarch64
David Monniaux
2020-04-10
1
-1
/
+7
|
*
|
|
use proper local labels
David Monniaux
2020-04-10
1
-1
/
+1
|
*
|
|
profiling still crashes on Aarch64
David Monniaux
2020-04-10
1
-1
/
+0
|
*
|
|
various fixes for aarch64 profiling
David Monniaux
2020-04-10
3
-1
/
+38
|
|
/
/
*
|
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-thread
David Monniaux
2020-04-08
7
-340
/
+751
|
\
|
|
|
*
|
disable leaf function removal of return address restoration due to memcpy ove...
David Monniaux
2020-03-27
3
-7
/
+13
|
*
|
Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work
David Monniaux
2020-03-27
3
-5
/
+38
|
|
\
\
|
|
*
|
better epilogue proof
David Monniaux
2020-03-25
1
-8
/
+18
|
|
*
|
removed RA restoration
David Monniaux
2020-03-25
3
-4
/
+27
|
*
|
|
Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work
David Monniaux
2020-03-26
2
-225
/
+532
|
|
\
|
|
|
|
*
|
RA is preserved
David Monniaux
2020-03-25
2
-18
/
+36
[next]