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
/
arm
Commit message (
Expand
)
Author
Age
Files
Lines
*
Implement support for big endian arm targets.
Bernhard Schommer
2016-08-05
5
-29
/
+60
*
Merge branch 'master' of /common/repositories/git/tools/compcert
Bernhard Schommer
2016-07-09
2
-0
/
+36
|
\
|
*
bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_...
Michael Schmidt
2016-07-08
2
-0
/
+36
*
|
Port to Coq 8.5pl2
Xavier Leroy
2016-07-08
4
-17
/
+14
|
/
*
Improved handling of "rotate left" and "rotate right" operators
Xavier Leroy
2016-06-22
1
-1
/
+1
*
Remove code that will is deprecated in ocaml 4.03
Bernhard Schommer
2016-06-21
2
-3
/
+3
*
fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can...
Michael Schmidt
2016-06-07
1
-1
/
+1
*
Introduce register pairs to describe calling conventions more precisely
Xavier Leroy
2016-05-17
3
-163
/
+156
*
bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are rest...
Michael Schmidt
2016-05-13
1
-1
/
+2
*
Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...
Xavier Leroy
2016-04-27
3
-272
/
+157
*
*/TargetPrinter.ml: wrong comment attached to Init_float32 constants
Xavier Leroy
2016-04-09
1
-1
/
+1
*
Merge branch 'master' into cleanup
Bernhard Schommer
2016-03-21
4
-64
/
+38
|
\
|
*
Merge pull request #93 from AbsInt/separate-compilation
Xavier Leroy
2016-03-20
2
-60
/
+34
|
|
\
|
|
*
Update the back-end proofs to the new linking framework.
Xavier Leroy
2016-03-06
1
-59
/
+33
|
|
*
Add support for EF_runtime externals
Xavier Leroy
2016-03-06
1
-1
/
+1
|
*
|
Print floating-point numbers with more digits in debug outputs
Xavier Leroy
2016-03-15
2
-4
/
+4
|
|
/
*
|
Added interface for the Asmexpansion.
Bernhard Schommer
2016-03-16
1
-4
/
+4
*
|
Cleanup of AsmToJSON.
Bernhard Schommer
2016-03-16
1
-0
/
+13
*
|
Deactivate warning 27 and added back removed code.
Bernhard Schommer
2016-03-15
3
-7
/
+8
*
|
Clean up of ia32 target dependend code.
Bernhard Schommer
2016-03-10
1
-2
/
+1
*
|
Cleanup of ARM dependedn code.
Bernhard Schommer
2016-03-10
2
-66
/
+8
|
/
*
bug 18168, catch cases where variadic arguments are transfered via registers
Michael Schmidt
2016-02-24
1
-2
/
+2
*
bug 18168, fix offset computation for var-args in ARM stacklayout
Michael Schmidt
2016-02-24
1
-1
/
+1
*
Do not use "movs rd, rs" nor "movs rd, #imm" in Thumb2 mode.
Xavier Leroy
2016-02-18
1
-2
/
+8
*
ARM: bug in expansion of __builtin_clzll
Xavier Leroy
2015-12-22
1
-1
/
+1
*
Add CLZ builtins for ARM and IA32
Xavier Leroy
2015-12-22
2
-1
/
+11
*
The return type of __builtin_clz() et al is "int", as documented and for GCC ...
v2.6
Xavier Leroy
2015-12-21
1
-1
/
+1
*
Print cfi_sections only if cfi is supported.
Bernhard Schommer
2015-12-15
1
-1
/
+1
*
Merge remote-tracking branch 'origin/master' into named-externals
Bernhard Schommer
2015-10-20
1
-8
/
+3
|
\
|
*
Fixed typos in the arm and ia32 section printing.
Bernhard Schommer
2015-10-16
1
-1
/
+1
|
*
Implemented the usage of DW_AT_ranges for non-contiguous address ranges.
Bernhard Schommer
2015-10-16
1
-0
/
+1
|
*
First step to implemente address ranges for the gnu backend.
Bernhard Schommer
2015-10-15
1
-7
/
+1
|
*
Use section type also for other targets.
Bernhard Schommer
2015-10-15
1
-2
/
+2
|
*
bug 17392: remove trailing whitespace in source files
Michael Schmidt
2015-10-14
14
-609
/
+609
|
*
bug 17392: remove trailing whitespace in source files
Michael Schmidt
2015-10-14
2
-49
/
+49
|
*
Implement the usage of the debug_str section for the gcc backend.
Bernhard Schommer
2015-10-13
1
-1
/
+1
*
|
Updated PR by removing whitespaces. Bug 17450.
Bernhard Schommer
2015-10-20
16
-658
/
+658
*
|
Use Coq strings instead of idents to name external and builtin functions.
Xavier Leroy
2015-10-11
2
-3
/
+3
|
/
*
Filled in missing functions for debug information on ia32.
Bernhard Schommer
2015-10-09
1
-23
/
+2
*
Filled in the rest of the funciton needed for thte debug info under arm.
Bernhard Schommer
2015-10-09
2
-9
/
+69
*
Added versions of the tranform_* functions in AST to work with functions
Bernhard Schommer
2015-10-08
1
-2
/
+2
*
Fixed minor typos in the comments.
Bernhard Schommer
2015-10-04
1
-1
/
+1
*
Add the forgotten Fileinfo also to arm and ia32 TargetPrinter.ml
Bernhard Schommer
2015-10-02
1
-0
/
+1
*
Cleanup of now no longer needed functions.
Bernhard Schommer
2015-10-01
1
-11
/
+1
*
Change the way the debug sections are printed.
Bernhard Schommer
2015-09-28
1
-1
/
+1
*
Added printing the reference address for the LocRef and started refactoring old
Bernhard Schommer
2015-09-27
1
-9
/
+1
*
Added support for the locations of stack allocated local variables.
Bernhard Schommer
2015-09-25
1
-0
/
+1
*
Record the scope structure during unblocking.
Bernhard Schommer
2015-09-22
1
-0
/
+2
*
Revert "Startet implementation of new Debug interface."
Bernhard Schommer
2015-09-10
1
-1
/
+0
*
Startet implementation of new Debug interface.
Bernhard Schommer
2015-09-06
1
-0
/
+1
[next]