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
...
*
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
*
Revised translation of '&&' and '||' to Clight.
Xavier Leroy
2014-10-13
11
-124
/
+109
*
Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.
Xavier Leroy
2014-10-09
3
-1
/
+3
*
Merge pull request #1 from jhjourdan/master
Xavier Leroy
2014-10-09
21
-942
/
+6030
|
\
|
*
Upgrade to flocq 2.4.0
Jacques-Henri Jourdan
2014-10-07
21
-942
/
+6030
*
|
Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ...
Bernhard Schommer
2014-10-08
1
-138
/
+220
*
|
Refactored the code of powerpc/PrintAsm.ml by moving the function depending o...
Bernhard Schommer
2014-10-08
1
-200
/
+236
|
/
*
Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ...
Bernhard Schommer
2014-10-06
1
-44
/
+86
*
Removed environment variable for the stdlib_path and added a new variable for...
Bernhard Schommer
2014-10-06
3
-20
/
+20
*
Change the way the tools like the linker, assembler, etc. are specified by in...
Bernhard Schommer
2014-09-30
4
-22
/
+113
*
Moved the timing facility to a seperate file.
Bernhard Schommer
2014-09-29
5
-54
/
+68
*
Refactoring in the printing of FP numbers.
Xavier Leroy
2014-09-24
1
-8
/
+2
*
Add theorem "elements_remove".
Xavier Leroy
2014-09-24
1
-167
/
+178
*
Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc).
Xavier Leroy
2014-09-24
1
-7
/
+20
*
GCCism: accept __volatile and __volatile__
Xavier Leroy
2014-09-21
1
-0
/
+2
*
Add .gitignore files.
Xavier Leroy
2014-09-21
6
-0
/
+63
*
Error instead of warning on illegal escape sequences.
Xavier Leroy
2014-09-21
2
-1
/
+5
*
Trim blank lines
v2.4
xleroy
2014-09-17
1
-2
/
+0
*
Update changelog and version for 2.4
xleroy
2014-09-17
2
-3
/
+4
*
Tolerance in parsing of 'section' pragma
xleroy
2014-09-17
1
-0
/
+3
*
Cold feet: suppress builtins for load with reservation/store conditional, use...
xleroy
2014-08-28
5
-47
/
+2
*
Update
xleroy
2014-08-28
1
-1
/
+2
*
Update for 2.4
xleroy
2014-08-27
1
-23
/
+37
*
Rename __builtin_cntlz to __builtin_clz.
xleroy
2014-08-27
11
-6
/
+25
*
More efficient implementations of map, fold, etc.
xleroy
2014-08-27
1
-164
/
+109
*
More careful detection of inlined builtins. Produces better error messages i...
xleroy
2014-08-25
1
-0
/
+1
*
Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false.
xleroy
2014-08-21
3
-5
/
+10
*
Support C99 compound literals (by expansion in Unblock pass).
xleroy
2014-08-21
16
-454
/
+801
*
Follow-up to commit 2613
xleroy
2014-08-20
1
-0
/
+2
*
Add builtins for load with reservation and conditional store.
xleroy
2014-08-20
5
-1
/
+39
*
Wrong types for strex builtins.
xleroy
2014-08-20
1
-4
/
+4
*
Better validation of target for ARM
xleroy
2014-08-20
1
-1
/
+5
*
Obvious typos in commit r2609
xleroy
2014-08-20
1
-8
/
+8
*
Add some more synchronization builtins
xleroy
2014-08-20
2
-1
/
+39
*
Improve error reporting for unsupported compound literals.
xleroy
2014-08-20
1
-1
/
+4
*
Excessively strict validation: ofs + sz < modulus should have been
xleroy
2014-08-20
1
-4
/
+5
*
Rename "-fthumb" option into "-mthumb" for GCC compatibility.
xleroy
2014-08-19
5
-18
/
+22
*
checklink/Check.ml: missing SDA addressing for store instructions.
xleroy
2014-08-19
5
-14
/
+217
*
Update dependencies
xleroy
2014-08-19
1
-14
/
+14
*
powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.
xleroy
2014-08-18
7
-124
/
+139
*
Improve error detection and error messages for enums.
xleroy
2014-08-17
1
-3
/
+7
*
Issue with switch labels that are negative 32-bit integers.
xleroy
2014-08-17
2
-4
/
+42
*
Add some tests for "switch" over 32 and 64-bit integers.
xleroy
2014-08-17
3
-1
/
+109
*
- Support "switch" statements over 64-bit integers
xleroy
2014-08-17
32
-709
/
+1220
[prev]
[next]