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 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
*
|
test/ : stop at first error in "make all"
Xavier Leroy
2017-08-26
1
-1
/
+1
*
|
test/: add a CCOMPOPTS make variable to pass additional compile-time flags
Xavier Leroy
2017-08-26
5
-5
/
+5
*
|
Reduce the running times of the tests in test/c
Xavier Leroy
2017-08-26
30
-87
/
+75
*
|
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
|
|
\
\
[prev]
[next]