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
*
PR#15: vararg functions are not eligible for inlining.
Xavier Leroy
2015-01-02
1
-1
/
+1
*
Translation of wide string literals.
Xavier Leroy
2015-01-01
1
-6
/
+57
*
Wrong handling of block-local function declarations (again)
Xavier Leroy
2015-01-01
1
-12
/
+7
*
Revised type compatibility check w.r.t. handling of attributes.
Xavier Leroy
2015-01-01
4
-49
/
+93
*
PR#12: regression introduced in commit 2d32afc
Xavier Leroy
2014-12-30
1
-2
/
+0
*
PR#6: fix handling of wchar_t and assignments from wide string literals.
Xavier Leroy
2014-12-30
5
-9
/
+31
*
PR#11: support sizeof(struct {...}) and _Alignof(struct {...})
Xavier Leroy
2014-12-30
1
-25
/
+38
*
Improve printing of errors.
Xavier Leroy
2014-12-30
1
-3
/
+11
*
PR#10 continued: disambiguate record to avoid OCaml warning
Xavier Leroy
2014-12-30
1
-1
/
+1
*
PR#10: composite definitions must be maintained in the environment.
Xavier Leroy
2014-12-30
1
-6
/
+15
*
cparser/Parser.v is generated.
Xavier Leroy
2014-12-30
1
-0
/
+1
*
Recognize more of GCC's alternate keywords (e.g. "__signed").
Xavier Leroy
2014-12-29
1
-21
/
+24
*
Support "asm volatile" (closes: PR#5).
Xavier Leroy
2014-12-29
2
-1
/
+3
*
One more cleanup in configure.
Xavier Leroy
2014-12-18
1
-1
/
+1
*
No longer include a pre-generated Parser.v in the distribution.
Xavier Leroy
2014-12-18
4
-61679
/
+15
*
Merge pull request #3 from AbsInt/pure-makefiles
Xavier Leroy
2014-12-18
8
-85
/
+371
|
\
|
*
Minor bug fixes in configure and Makefile.extr
Xavier Leroy
2014-12-17
2
-5
/
+6
|
*
Merge branch 'master' into pure-makefiles
Xavier Leroy
2014-12-17
59
-763
/
+2379
|
|
\
|
|
/
|
/
|
*
|
Clean up support for common symbols. Uninitialized "const" symbols can be co...
Xavier Leroy
2014-12-17
6
-39
/
+71
*
|
Use cp instead of symbolic links for executables.
Xavier Leroy
2014-12-17
1
-15
/
+8
*
|
Merge branch 'master' of https://github.com/AbsInt/CompCert
Xavier Leroy
2014-12-17
5
-19
/
+35
|
\
\
|
*
|
Stdlib path is ignored when the configuration has_runtime_lib is set to false.
Bernhard Schommer
2014-12-15
1
-2
/
+7
|
*
|
Update the IA32/MacOS X port.
Xavier Leroy
2014-12-11
2
-5
/
+7
|
*
|
Prevent constant propagation on Oindirectsymbol addresses.
Xavier Leroy
2014-12-11
1
-2
/
+11
|
*
|
Preserve single quotes (e.g. in CPREPRO) when generating compcert.ini
Xavier Leroy
2014-12-11
1
-10
/
+10
*
|
|
Prototype the pointer so that the program has well defined semantics and pass...
Xavier Leroy
2014-12-17
1
-1
/
+1
|
/
/
*
|
Removed more unused variables.
Bernhard Schommer
2014-12-04
1
-1
/
+0
*
|
Removed unused variable and changed the search for the installation directory...
Bernhard Schommer
2014-12-04
2
-6
/
+1
*
|
Changed the comparison of jumptables.
Bernhard Schommer
2014-12-01
1
-14
/
+7
*
|
Wrong handling of block-local function declarations (in Elab.ml).
Xavier Leroy
2014-11-26
4
-13
/
+31
*
|
Use Bitstring.is_zeroes_bitstring from bitstring 2.0.4.
Xavier Leroy GALLIUM
2014-11-25
1
-0
/
+8
*
|
Merge pull request #2 from AbsInt/public-globals
Xavier Leroy
2014-11-25
43
-660
/
+2206
|
\
\
|
*
|
Update the ARM port.
Xavier Leroy
2014-11-24
2
-50
/
+38
|
*
|
Update PowerPC port.
Xavier Leroy
2014-11-24
2
-21
/
+51
|
*
|
Verification of the Unusedglob pass (removal of unreferenced static global de...
Xavier Leroy
2014-11-24
12
-264
/
+1458
|
*
|
Add Genv.public_symbol operation.
Xavier Leroy
2014-11-24
24
-263
/
+562
|
*
|
Record public global definitions via field "prog_public" in AST.program.
Xavier Leroy
2014-11-24
7
-63
/
+98
|
/
/
*
|
Use gettimeofday() instead of obsolete ftime().
Xavier Leroy
2014-11-24
2
-11
/
+19
|
*
Use OCaml's .opt compilers when available.
Xavier Leroy
2014-12-17
3
-32
/
+82
|
*
Remove ocamlbuild configuration files, no longer used.
Xavier Leroy
2014-11-22
2
-23
/
+0
|
*
Use String.map instead of reimplementing it ourselves.
Xavier Leroy
2014-11-22
1
-5
/
+18
|
*
Replace ocamlbuild by a second-stage makefile to compile the OCaml code and p...
Xavier Leroy
2014-11-22
5
-59
/
+296
|
/
*
Analysis of jump tables was using the wrong size.
Xavier Leroy
2014-11-17
1
-1
/
+1
*
Add flags to control individual optimization passes + flag -O0 for turning th...
Xavier Leroy
2014-11-16
7
-46
/
+128
*
Revised parsing of command-line arguments (in preparation for adding more).
Xavier Leroy
2014-11-16
3
-118
/
+250
*
build_from_parsed: simplified code + correctness proof.
Xavier Leroy
2014-11-15
1
-15
/
+86
*
cchecklink: added option "-files-from" to read .sdump file names
Xavier Leroy
2014-11-15
2
-4
/
+29
*
Tune behavior wrt warnings:
Xavier Leroy
2014-10-24
2
-2
/
+3
*
Deactivated the warning for deprecated features for compilation of cchecklink...
Bernhard Schommer
2014-10-20
1
-0
/
+1
*
Removed duplicated open.
Bernhard Schommer
2014-10-17
1
-1
/
+0
[next]