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
*
Merge branch 'master' into dwarf
Bernhard Schommer
2015-01-12
1
-3
/
+6
|
\
|
*
More prudent analysis of uninitialized const global variables.
Xavier Leroy
2015-01-09
1
-3
/
+6
*
|
Merge branch 'master' into dwarf
Bernhard Schommer
2015-01-12
34
-61988
/
+914
|
\
|
|
*
In -g -S mode, annotate the generated asm file with the C source code in comm...
Xavier Leroy
2015-01-07
6
-86
/
+243
|
*
PR#19: there is no reason to reject an empty "switch" statement.
Xavier Leroy
2015-01-06
1
-2
/
+0
|
*
PR#16: give option rules precedence over file pattern rules.
Xavier Leroy
2015-01-03
3
-31
/
+38
|
*
PR#14: recognize ".so" arguments as files to pass to the linker.
Xavier Leroy
2015-01-02
1
-1
/
+2
|
*
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
|
|
|
\
|
|
|
/
|
|
/
|
|
|
*
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
*
|
|
Added dummy printing function for entries.
Bernhard Schommer
2014-12-18
1
-1
/
+4
*
|
|
Merge branch 'master' into dwarf
Bernhard Schommer
2014-12-17
10
-58
/
+88
|
\
|
|
|
*
|
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
|
*
|
|
Prototype the pointer so that the program has well defined semantics and pass...
Xavier Leroy
2014-12-17
1
-1
/
+1
*
|
|
|
Added more printing code.
Bernhard Schommer
2014-12-15
1
-3
/
+8
*
|
|
|
Started implementation of printing the dwarf entries.
Bernhard Schommer
2014-12-15
3
-11
/
+31
*
|
|
|
Merge branch 'master' into dwarf
Bernhard Schommer
2014-12-11
4
-17
/
+28
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
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
|
|
/
/
*
|
|
Merge branch 'master' into dwarf
Bernhard Schommer
2014-12-04
1
-1
/
+0
|
\
|
|
|
*
|
Removed more unused variables.
Bernhard Schommer
2014-12-04
1
-1
/
+0
*
|
|
Merge branch 'master' into dwarf
Bernhard Schommer
2014-12-04
2
-6
/
+1
|
\
|
|
|
*
|
Removed unused variable and changed the search for the installation directory...
Bernhard Schommer
2014-12-04
2
-6
/
+1
*
|
|
Changed the d1line and d1file to d2line and d2file and prologue and epilogue ...
Bernhard Schommer
2014-12-04
5
-9
/
+79
*
|
|
Merge branch 'master' into dwarf
Bernhard Schommer
2014-12-02
1
-14
/
+7
|
\
|
|
|
*
|
Changed the comparison of jumptables.
Bernhard Schommer
2014-12-01
1
-14
/
+7
*
|
|
Renamed the printer module for the Abbreviations and deactivated adding the -...
Bernhard Schommer
2014-12-02
3
-47
/
+11
[next]