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
path:
root
/
common
Commit message (
Expand
)
Author
Age
Files
Lines
*
Put forward_simulation and backward_simulation in Prop instead of Type
Xavier Leroy
2016-03-06
2
-303
/
+323
*
Add support for EF_runtime externals
Xavier Leroy
2016-03-06
2
-52
/
+33
*
Globalenvs: adapt to new linking framework, and revise.
Xavier Leroy
2016-03-06
1
-1146
/
+729
*
AST: extend and adapt to the new linking framework.
Xavier Leroy
2016-03-06
1
-460
/
+116
*
The basic framework for linking and separate compilation.
Xavier Leroy
2016-03-06
1
-0
/
+905
*
Preliminaries: minor extensions to Memory
Xavier Leroy
2016-03-06
1
-3
/
+58
*
Merge remote-tracking branch 'origin/master' into named-externals
Bernhard Schommer
2015-10-20
2
-4
/
+8
|
\
|
*
Implemented the usage of DW_AT_ranges for non-contiguous address ranges.
Bernhard Schommer
2015-10-16
2
-0
/
+2
|
*
bug 17392: remove trailing whitespace in source files
Michael Schmidt
2015-10-14
14
-1666
/
+1666
|
*
bug 17392: remove trailing whitespace in source files
Michael Schmidt
2015-10-14
3
-8
/
+8
|
*
Changed the type of the debug sections with additional string.
Bernhard Schommer
2015-10-13
2
-4
/
+4
|
*
Implement the usage of the debug_str section for the gcc backend.
Bernhard Schommer
2015-10-13
2
-2
/
+4
*
|
Updated PR by removing whitespaces. Bug 17450.
Bernhard Schommer
2015-10-20
17
-1673
/
+1673
*
|
Use Coq strings instead of idents to name external and builtin functions.
Xavier Leroy
2015-10-11
4
-25
/
+23
|
/
*
Filled in the rest of the funciton needed for thte debug info under arm.
Bernhard Schommer
2015-10-09
2
-0
/
+2
*
Added versions of the tranform_* functions in AST to work with functions
Bernhard Schommer
2015-10-08
1
-1
/
+216
*
Change the way the debug sections are printed.
Bernhard Schommer
2015-09-28
2
-2
/
+2
*
Added support for the locations of stack allocated local variables.
Bernhard Schommer
2015-09-25
2
-0
/
+2
*
Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.
Xavier Leroy
2015-08-22
3
-16
/
+16
*
Refactoring of builtins and annotations in the back-end.
Xavier Leroy
2015-08-21
3
-358
/
+297
*
Represent external worlds by a coinductive type rather than an inductive type.
Xavier Leroy
2015-06-07
1
-1
/
+1
*
In AST.calling_conventions, record whether the original C function was "old-s...
Xavier Leroy
2015-05-22
1
-3
/
+4
*
Extended inline asm: revised treatment of clobbered registers.
Xavier Leroy
2015-05-09
1
-2
/
+2
*
Typo: Val.sun_inject -> Val.sub_inject.
Xavier Leroy
2015-05-06
1
-1
/
+1
*
Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...
Xavier Leroy
2015-04-30
5
-111
/
+113
*
Support for GCC-style extended asm, continued:
Xavier Leroy
2015-04-21
3
-5
/
+6
*
Experiment: support a subset of GCC's extended asm statements.
Xavier Leroy
2015-04-17
3
-8
/
+8
*
Merge branch 'master' into dwarf
Bernhard Schommer
2015-04-02
4
-46
/
+249
|
\
|
*
Merge pull request #34 from AbsInt/extended-annotations
Xavier Leroy
2015-04-01
4
-29
/
+216
|
|
\
|
|
*
Updated the Caml part. Added some more tests in annot1.c.
Xavier Leroy
2015-03-27
1
-2
/
+4
|
|
*
Extended arguments to annotations, continued:
Xavier Leroy
2015-03-27
2
-34
/
+6
|
|
*
Extend annotations so that they can keep track of global variables and local ...
Xavier Leroy
2015-03-27
3
-29
/
+242
|
*
|
Revised semantics of comparisons between a pointer and 0.
Xavier Leroy
2015-03-15
1
-17
/
+33
|
|
/
*
|
Started integrating the debug printing in the common backend_printer.
Bernhard Schommer
2015-03-11
2
-2
/
+2
*
|
Starting to remove the seperate printers for each backend.
Bernhard Schommer
2015-02-02
2
-0
/
+4
|
/
*
Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.
Xavier Leroy
2015-01-23
1
-70
/
+122
*
Merge branch 'named-structs'
Xavier Leroy
2015-01-23
4
-177
/
+260
|
\
|
*
Make small-step semantics more parametric w.r.t. the type of global environme...
Xavier Leroy
2014-11-26
2
-27
/
+42
|
*
Introduce symbol environments (type Senv.t) as a restricted view on global en...
Xavier Leroy
2014-11-26
2
-150
/
+218
*
|
Clean up support for common symbols. Uninitialized "const" symbols can be co...
Xavier Leroy
2014-12-17
2
-8
/
+8
|
/
*
Add Genv.public_symbol operation.
Xavier Leroy
2014-11-24
4
-180
/
+342
*
Record public global definitions via field "prog_public" in AST.program.
Xavier Leroy
2014-11-24
1
-3
/
+25
*
Excessively strict validation: ofs + sz < modulus should have been
xleroy
2014-08-20
1
-4
/
+5
*
Issue with switch labels that are negative 32-bit integers.
xleroy
2014-08-17
1
-0
/
+35
*
- Support "switch" statements over 64-bit integers
xleroy
2014-08-17
2
-171
/
+264
*
Add Mem.free_parallel_inject and use it to simplify Events a bit.
xleroy
2014-07-31
3
-35
/
+50
*
Update "read_as_zeros" property.
xleroy
2014-07-23
1
-1
/
+3
*
Merge of "newspilling" branch:
xleroy
2014-07-23
8
-504
/
+602
*
Add "read_as_zero" property for memory areas initialized by Init_space.
xleroy
2014-06-30
1
-14
/
+106
*
Refactoring: move symbol_offset into Genv.
xleroy
2014-05-24
1
-0
/
+17
[next]