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
Commit message (
Expand
)
Author
Age
Files
Lines
*
Prefixed runtime functions.
Bernhard Schommer
2017-08-25
60
-269
/
+269
*
Document -finline in help.
Bernhard Schommer
2017-08-24
1
-0
/
+1
*
Fixed typo.
Bernhard Schommer
2017-08-24
1
-1
/
+1
*
Extended support for the nostartfiles option.
Bernhard Schommer
2017-08-23
1
-6
/
+11
*
ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudo, continued
Xavier Leroy
2017-08-22
1
-1
/
+2
*
ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudo
Xavier Leroy
2017-08-22
2
-6
/
+7
*
Issue P #25: make sure sizeof(long double) = sizeof(double) in all contexts.
Xavier Leroy
2017-08-22
2
-10
/
+12
*
Update documentation index for release 3.1
v3.1
Xavier Leroy
2017-08-18
1
-23
/
+17
*
Merge remote-tracking branch 'private/master'
Xavier Leroy
2017-08-18
8
-91
/
+201
|
\
|
*
Merge pull request #22 from AbsIntPrivate/arm_large_offsets
Xavier Leroy
2017-08-18
8
-91
/
+201
|
|
\
|
|
*
ARM: tweak stack layout so that back link and return address are lower
Xavier Leroy
2017-08-17
1
-37
/
+34
|
|
*
ARM port: replace Psavelr pseudo-instruction by actual instructions
Xavier Leroy
2017-08-17
6
-47
/
+88
|
|
*
Asmgenproof0: some more useful lemmas
Xavier Leroy
2017-08-17
1
-0
/
+29
|
|
*
ARM: Generate Pcfi_rel_offset directives directly from Asmgen
Xavier Leroy
2017-08-17
4
-12
/
+17
|
|
*
Push correct register
Michael Schmidt
2017-08-02
1
-1
/
+1
|
|
*
Improve stack offset addressing
Michael Schmidt
2017-08-02
5
-35
/
+73
*
|
|
configure: Wording and formatting of the Skylake/OCaml warning
Xavier Leroy
2017-08-18
1
-2
/
+3
*
|
|
Update Changelog in preparation for release 3.1
Xavier Leroy
2017-08-18
1
-2
/
+8
|
/
/
*
/
Issue #196: excessive proof-checking times in .v files generated by clightgen
Xavier Leroy
2017-08-15
3
-13
/
+34
|
/
*
Merge branch 'master' of github.com:AbsInt/CompCert
Bernhard Schommer
2017-07-31
1
-1
/
+3
|
\
|
*
Mention rv32- and rv64- configurations in the help message
Xavier Leroy
2017-07-31
1
-0
/
+2
|
*
Accept Coq version 8.6.1 as supported
Xavier Leroy
2017-07-31
1
-1
/
+1
*
|
Warning for Skylake/Kabylake systems.
Bernhard Schommer
2017-07-31
1
-0
/
+4
|
/
*
Merge branch 'master' of github.com:AbsIntPrivate/CompCert
Bernhard Schommer
2017-07-27
1
-20
/
+27
|
\
|
*
use TMPDIR also for asm-cfi test
Michael Schmidt
2017-07-27
1
-5
/
+5
|
*
generalize test for compiler options
Michael Schmidt
2017-07-27
1
-15
/
+22
*
|
Update Changelog with news since release 3.0.1
Xavier Leroy
2017-07-27
1
-4
/
+29
|
/
*
Integrated fixup code in estimated size.
Bernhard Schommer
2017-07-26
1
-0
/
+3
*
Added annot to json dump.
Bernhard Schommer
2017-07-24
1
-3
/
+20
*
Print_annot should produce a string.
Bernhard Schommer
2017-07-19
5
-40
/
+54
*
No verbose debug info in default mode.
Bernhard Schommer
2017-07-14
1
-5
/
+17
*
Update documentation entry point for release 3.0 (retroactively)
Xavier Leroy
2017-07-13
1
-5
/
+8
*
Constprop strength reduction (#17)
Bernhard Schommer
2017-07-12
4
-16
/
+325
*
SimlLocals.Sdebug_var: wrong type for 64-bit platforms
Xavier Leroy
2017-07-09
1
-1
/
+1
*
Add a -ignore-coq-version flag to configure (continued)
Xavier Leroy
2017-07-06
1
-2
/
+2
*
Extend builtin arguments with a pointer addition operator, continued
Xavier Leroy
2017-07-06
18
-99
/
+283
*
Extend builtin arguments with a pointer addition operator
Xavier Leroy
2017-07-06
29
-37
/
+211
*
Issue #16P: wrong rlwinm instruction generated by constant propagation
Xavier Leroy
2017-07-05
3
-13
/
+30
*
Merge branch 'master' of github.com:AbsIntPrivate/CompCert
Bernhard Schommer
2017-07-05
1
-0
/
+30
|
\
|
*
Merge pull request #14 from AbsIntPrivate/configure_no_pie
Michael Schmidt
2017-07-05
1
-0
/
+30
|
|
\
|
|
*
add check for -no-pie at configure-time
Michael Schmidt
2017-07-04
1
-0
/
+30
|
|
/
*
|
Add a -ignore-coq-version flag to configure (continued)
Xavier Leroy
2017-07-05
1
-1
/
+1
*
|
Add a -ignore-coq-version flag to configure
Xavier Leroy
2017-07-05
1
-2
/
+10
|
/
*
Adopted section names in AsmToJson.
Bernhard Schommer
2017-06-29
1
-10
/
+23
*
Revert "Update git ignore spec"
Bernhard Schommer
2017-06-28
1
-1
/
+0
*
Merge branch 'master' of /common/repositories/git/tools/compcert
Bernhard Schommer
2017-06-28
1
-0
/
+1
|
\
|
*
Update git ignore spec
Markus Pister
2017-06-28
1
-0
/
+1
*
|
Formatted json printing.
Bernhard Schommer
2017-06-28
9
-353
/
+370
|
/
*
Added a little bit more compilation info to sdump.
Bernhard Schommer
2017-06-26
3
-4
/
+16
*
Added pseudo instruction for inline asm.
Bernhard Schommer
2017-06-20
1
-0
/
+15
[next]