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
...
|
*
|
Some "feel good" proofs about avail sets.
Xavier Leroy
2015-08-23
1
-0
/
+171
|
*
|
Track the locations of local variables using EF_debug annotations.
Xavier Leroy
2015-08-23
12
-45
/
+1030
|
*
|
Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.
Xavier Leroy
2015-08-22
27
-125
/
+114
|
*
|
Adapt the PowerPC port to the new builtin representation.
Xavier Leroy
2015-08-21
11
-260
/
+285
|
*
|
Simplify the handling of extended inline asm, taking advantage of the new, st...
Xavier Leroy
2015-08-21
3
-14
/
+30
|
*
|
Merge branch 'master' into 'new-builtins'
Xavier Leroy
2015-08-21
12
-185
/
+206
|
|
\
\
|
*
|
|
Refactoring of builtins and annotations in the back-end.
Xavier Leroy
2015-08-21
64
-2044
/
+2181
*
|
|
|
Improve printing of internal compiler errors.
Xavier Leroy
2015-08-25
1
-2
/
+2
*
|
|
|
Fixed the -T option.
Bernhard Schommer
2015-08-25
1
-1
/
+1
*
|
|
|
Fixed abbreviation of DW_TAG_formal_parameter.
Bernhard Schommer
2015-08-25
1
-1
/
+1
*
|
|
|
Fixed error in handling of anonymous struct/union/enum types.
Bernhard Schommer
2015-08-24
1
-8
/
+15
*
|
|
|
Also change the order of high and low pc in the compilation unit tag.
Bernhard Schommer
2015-08-24
1
-1
/
+1
*
|
|
|
Count number of input files and do not use number of source files for warning...
Bernhard Schommer
2015-08-24
1
-12
/
+14
*
|
|
|
Added error message when no input file is specified.
Bernhard Schommer
2015-08-23
1
-0
/
+5
*
|
|
|
Revert "Added support for the location of non static global variables."
Bernhard Schommer
2015-08-23
3
-9
/
+2
*
|
|
|
Do not add subsize tag to array types without size such as flexible array me...
Bernhard Schommer
2015-08-23
1
-10
/
+14
*
|
|
|
Added the directory ../share/compcert to the search path for .ini files and r...
Bernhard Schommer
2015-08-23
1
-9
/
+12
|
|
/
/
|
/
|
|
*
|
|
test/regression: test packedstruct1 only if unaligned accesses are supported.
Xavier Leroy
2015-08-21
5
-6
/
+15
*
|
|
Erase incomplete file .depend.extr if "make depend" fails.
Xavier Leroy
2015-08-21
1
-3
/
+2
*
|
|
Don't use strdup(), it is not ISO C99.
Xavier Leroy
2015-08-21
1
-1
/
+2
*
|
|
Asmexpand for ARM: fixed bug in Pfreeframe.
Xavier Leroy
2015-08-21
2
-5
/
+5
*
|
|
Fix bugs in Asmexpand.ml for ARM.
Xavier Leroy
2015-08-21
1
-8
/
+9
*
|
|
Consistent naming of "P" instructions and consistent ordering of arguments
Xavier Leroy
2015-08-21
3
-174
/
+171
|
|
/
|
/
|
*
|
Fixed bugs in asm expansion causing the test suite to fail.
Xavier Leroy
2015-08-21
1
-13
/
+20
*
|
Added command line option to specify a linker command file for the linker.
Bernhard Schommer
2015-08-20
1
-0
/
+5
|
/
*
Added support for the location of non static global variables.
Bernhard Schommer
2015-08-18
3
-2
/
+9
*
Added builtin for the dcbf instruction
Bernhard Schommer
2015-08-17
5
-0
/
+9
*
Merge pull request #46 from AbsInt/asmexpand
Xavier Leroy
2015-08-17
8
-615
/
+1031
|
\
|
*
Merge branch 'master' into asmexpand
Bernhard Schommer
2015-07-14
1
-1
/
+4
|
|
\
|
*
|
Updated the branch and implemented the suggested changes.
Bernhard Schommer
2015-07-14
3
-44
/
+78
|
*
|
Merge branch 'master' into asmexpand
Bernhard Schommer
2015-07-14
51
-241
/
+1046
|
|
\
\
|
*
|
|
Merge branch 'asmexpand' of github.com:AbsInt/CompCert
Bernhard Schommer
2015-06-26
8
-615
/
+997
*
|
|
|
Added builtin for the dcbi instruction.
Bernhard Schommer
2015-08-17
5
-4
/
+11
*
|
|
|
Update clightgen w.r.t. teh calling_conventions record (new field cc_unproto).
Xavier Leroy
2015-08-17
1
-1
/
+2
*
|
|
|
Update clightgen w.r.t. EF_inline_asm (type of the clobber list).
Xavier Leroy
2015-08-17
1
-1
/
+6
*
|
|
|
Added builitin for the icbi instruction.
Bernhard Schommer
2015-08-14
5
-1
/
+11
*
|
|
|
Added builtin for the lwsync barrier.
Bernhard Schommer
2015-08-14
5
-3
/
+12
*
|
|
|
Also print the system in the output to differentiate between diab and gcc pro...
Bernhard Schommer
2015-08-05
1
-2
/
+2
*
|
|
|
Swapped high and low pc in the printing of the debug information for subrouti...
Bernhard Schommer
2015-07-24
1
-2
/
+2
*
|
|
|
More tests for alias analysis.
Xavier Leroy
2015-07-20
2
-6
/
+30
*
|
|
|
ValueDomain: add some documentation comments.
Xavier Leroy
2015-07-19
1
-20
/
+32
*
|
|
|
Test to check that alias analysis is prudently conservative on ill-defined po...
Xavier Leroy
2015-07-19
3
-1
/
+153
*
|
|
|
Value analysis: keep track of pointer values that leak through small integers...
Xavier Leroy
2015-07-19
9
-232
/
+250
*
|
|
|
Value analysis: keep track of pointer values that leak through arithmetic ope...
Xavier Leroy
2015-07-19
5
-163
/
+171
*
|
|
|
ValueDomain.aptr_of_aval: be more conservative with pointers synthesized from...
Xavier Leroy
2015-07-18
2
-6
/
+14
*
|
|
|
Missing cases in ValueDomain.vnormalize, causing overapproximation.
Xavier Leroy
2015-07-18
1
-2
/
+2
*
|
|
|
Missing case in ValueDomain.pincl, causing incompleteness.
Xavier Leroy
2015-07-18
1
-0
/
+9
*
|
|
|
Remove non digit and non letter chars from filename used in renaming of stati...
Bernhard Schommer
2015-07-15
1
-0
/
+1
*
|
|
|
Introduce tolerance for casts of pointer values to/from 64-bit integers.
Xavier Leroy
2015-07-15
1
-3
/
+12
|
|
_
|
/
|
/
|
|
*
|
|
Reject incomplete types as return type.
Bernhard Schommer
2015-07-14
1
-1
/
+4
|
|
/
|
/
|
[prev]
[next]