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
...
|
*
Remove temporary .o files after linking (#36)
Xavier Leroy
2017-11-27
1
-2
/
+5
*
|
Remove temporary .o files after linking (#36)
Xavier Leroy
2017-11-27
1
-2
/
+5
|
/
*
Issue #208: make value analysis of comparisons more conservative w.r.t. point...
Xavier Leroy
2017-11-24
2
-8
/
+15
*
Pull request #192: improve the printing of Clight intermediate code
Xavier Leroy
2017-11-22
3
-10
/
+29
*
Added json export for the abstract ARM Assembler
Bernhard Schommer
2017-11-20
2
-64
/
+338
*
Moved arm eabi fixup to Asmexpand.
Bernhard Schommer
2017-11-16
3
-159
/
+229
*
New json printing interface.
Bernhard Schommer
2017-11-14
4
-144
/
+208
*
Remove no longer used function. Bug 22525
Bernhard Schommer
2017-11-10
5
-8
/
+0
*
Removed no longer used function. Bug 22525
Bernhard Schommer
2017-11-09
5
-105
/
+1
*
Use address for printing address constant. Bug 22525
Bernhard Schommer
2017-11-09
1
-2
/
+3
*
Generalize print_init.
Bernhard Schommer
2017-11-09
1
-1
/
+40
*
Fix jumptable issue.
Bernhard Schommer
2017-11-08
4
-5
/
+8
*
Simplifiy handling of constant emmitting.
Bernhard Schommer
2017-11-08
4
-92
/
+71
*
Remove superfluous function.
Bernhard Schommer
2017-11-06
6
-11
/
+2
*
Also quote \a.
Bernhard Schommer
2017-10-26
1
-0
/
+2
*
Fix register name of ais printing and moved label function up.
Bernhard Schommer
2017-10-25
1
-4
/
+4
*
Remove ais_annot_intval.
Bernhard Schommer
2017-10-24
1
-13
/
+0
*
Prefix ais annotations with location.
Bernhard Schommer
2017-10-24
1
-2
/
+4
*
Coq 8.7.0 support
Xavier Leroy
2017-10-20
2
-3
/
+8
*
Merge pull request #191 from sigurdschneider/master
Xavier Leroy
2017-10-20
15
-3
/
+15
|
\
|
*
Ensure FunInd or Recdef is imported if functional induction is used
Sigurd Schneider
2017-07-20
15
-3
/
+15
*
|
New support for inserting ais-annotations.
Bernhard Schommer
2017-10-19
31
-66
/
+180
*
|
Check recursively for const for modifiable lvalues (#32)
Bernhard Schommer
2017-10-17
1
-2
/
+15
*
|
Do not generate object files for linking.
Bernhard Schommer
2017-10-16
1
-7
/
+14
*
|
Distinguish between long and int for cases.
Bernhard Schommer
2017-10-13
1
-7
/
+7
*
|
Make the list unique. Bug 22239
Bernhard Schommer
2017-09-26
1
-177
/
+22
*
|
Moved common buitlins to C2C gernic_builtins.
Bernhard Schommer
2017-09-26
5
-34
/
+11
*
|
Merge branch 'master' of github.com:AbsIntPrivate/CompCert
Bernhard Schommer
2017-09-25
0
-0
/
+0
|
\
\
|
*
|
Remove coq warnings (#28)
Bernhard Schommer
2017-09-22
72
-638
/
+638
*
|
|
Added dump-mnemonics option.
Bernhard Schommer
2017-09-25
8
-2
/
+208
*
|
|
Remove coq warnings (#28)
Bernhard Schommer
2017-09-22
72
-638
/
+638
|
/
/
*
|
Disallow usage of default pattern for AsmToJSON.
Bernhard Schommer
2017-09-22
1
-2
/
+11
*
|
Update version to 3.1
Michael Schmidt
2017-09-21
1
-1
/
+1
*
|
Some lemmas.
Bernhard Schommer
2017-09-21
1
-0
/
+14
*
|
Typo in Makefile: "ia32" is now "x86"
Xavier Leroy
2017-09-19
1
-1
/
+1
*
|
Reverted reintroduced quote of compilation dir.
Bernhard Schommer
2017-09-19
1
-2
/
+2
*
|
Deadcode: eliminate trivial Icond instructions
Xavier Leroy
2017-09-18
2
-2
/
+9
*
|
Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)
Gergö Barany
2017-09-18
9
-21
/
+43
*
|
Merge pull request #202 from gergo-/mla-folding
Xavier Leroy
2017-09-15
2
-0
/
+102
|
\
\
|
*
|
Strength reduction patterns for ARM mla instruction.
Gergö Barany
2017-09-15
2
-0
/
+102
|
/
/
*
|
Update the Cygwin x86-32 port
Xavier Leroy
2017-09-12
1
-10
/
+11
*
|
configure for x86-32/Cygwin: ignore __attribute__
Xavier Leroy
2017-09-11
1
-1
/
+1
*
|
Resurrect the Cygwin x86-32 port
Xavier Leroy
2017-09-11
2
-2
/
+60
*
|
test/*/Makefile: suppress dependencies on ../../ccomp
Xavier Leroy
2017-09-11
2
-6
/
+6
*
|
Makefile: chmod a-w instead of chmod -w
Xavier Leroy
2017-09-11
1
-1
/
+1
*
|
Issue #199: improve namespace management for clightgen-produced files
Xavier Leroy
2017-08-28
2
-16
/
+6
*
|
For running tests with the interpreter, use the correct -stdlib option
Xavier Leroy
2017-08-28
1
-3
/
+2
*
|
test/compression: use unique temporary files for testing
Xavier Leroy
2017-08-27
1
-7
/
+7
*
|
riscV/Conventions1: in 32-bit mode, wrong size for stack-allocated arguments ...
Xavier Leroy
2017-08-26
1
-2
/
+5
*
|
riscV/Machregs: no printable name was associated to register X31
Xavier Leroy
2017-08-26
1
-1
/
+1
[prev]
[next]