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
/
backend
/
SplitLongproof.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Replace `omega` tactic with `lia`
Xavier Leroy
2020-12-29
1
-15
/
+15
*
Give formal semantics to some built-in functions and run-time functions
Xavier Leroy
2019-07-17
1
-72
/
+61
*
Prefixed runtime functions.
Bernhard Schommer
2017-08-25
1
-30
/
+30
*
Hybrid 64bit/32bit PowerPC port
Bernhard Schommer
2017-05-03
1
-10
/
+10
*
Use "Local" as prefix
Xavier Leroy
2017-02-13
1
-2
/
+2
*
Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...
Xavier Leroy
2016-10-27
1
-6
/
+6
*
SplitLong: propagate constants through "longofint"
Xavier Leroy
2016-10-25
1
-2
/
+3
*
Update ARM port. Not tested yet.
Xavier Leroy
2016-10-25
1
-1
/
+1
*
Turn 64-bit integer division and modulus by constants into multiply-high
Xavier Leroy
2016-10-04
1
-2
/
+20
*
Finish the proofs of SelectLong for IA32
Xavier Leroy
2016-10-02
1
-1
/
+1
*
Improve code generation for 64-bit signed integer division
Xavier Leroy
2016-10-02
1
-86
/
+47
*
Support for 64-bit architectures: generic support
Xavier Leroy
2016-10-01
1
-0
/
+1142