aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-269-201/+245
* Use Bitstring.is_zeroes_bitstring from bitstring 2.0.4.Xavier Leroy GALLIUM2014-11-251-0/+8
* Merge pull request #2 from AbsInt/public-globalsXavier Leroy2014-11-2543-660/+2206
|\
| * Update the ARM port.Xavier Leroy2014-11-242-50/+38
| * Update PowerPC port.Xavier Leroy2014-11-242-21/+51
| * Verification of the Unusedglob pass (removal of unreferenced static global de...Xavier Leroy2014-11-2412-264/+1458
| * Add Genv.public_symbol operation.Xavier Leroy2014-11-2424-263/+562
| * Record public global definitions via field "prog_public" in AST.program.Xavier Leroy2014-11-247-63/+98
|/
* Use gettimeofday() instead of obsolete ftime().Xavier Leroy2014-11-242-11/+19
* Analysis of jump tables was using the wrong size.Xavier Leroy2014-11-171-1/+1
* Add flags to control individual optimization passes + flag -O0 for turning th...Xavier Leroy2014-11-167-46/+128
* Revised parsing of command-line arguments (in preparation for adding more).Xavier Leroy2014-11-163-118/+250
* build_from_parsed: simplified code + correctness proof.Xavier Leroy2014-11-151-15/+86
* cchecklink: added option "-files-from" to read .sdump file namesXavier Leroy2014-11-152-4/+29
* Tune behavior wrt warnings:Xavier Leroy2014-10-242-2/+3
* Deactivated the warning for deprecated features for compilation of cchecklink...Bernhard Schommer2014-10-201-0/+1
* Removed duplicated open.Bernhard Schommer2014-10-171-1/+0
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-1311-124/+109
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-093-1/+3
* Merge pull request #1 from jhjourdan/masterXavier Leroy2014-10-0921-942/+6030
|\
| * Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-0721-942/+6030
* | Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ...Bernhard Schommer2014-10-081-138/+220
* | Refactored the code of powerpc/PrintAsm.ml by moving the function depending o...Bernhard Schommer2014-10-081-200/+236
|/
* Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ...Bernhard Schommer2014-10-061-44/+86
* Removed environment variable for the stdlib_path and added a new variable for...Bernhard Schommer2014-10-063-20/+20
* Change the way the tools like the linker, assembler, etc. are specified by in...Bernhard Schommer2014-09-304-22/+113
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-295-54/+68
* Refactoring in the printing of FP numbers.Xavier Leroy2014-09-241-8/+2
* Add theorem "elements_remove".Xavier Leroy2014-09-241-167/+178
* Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc).Xavier Leroy2014-09-241-7/+20
* GCCism: accept __volatile and __volatile__Xavier Leroy2014-09-211-0/+2
* Add .gitignore files.Xavier Leroy2014-09-216-0/+63
* Error instead of warning on illegal escape sequences.Xavier Leroy2014-09-212-1/+5
* Trim blank linesv2.4xleroy2014-09-171-2/+0
* Update changelog and version for 2.4xleroy2014-09-172-3/+4
* Tolerance in parsing of 'section' pragmaxleroy2014-09-171-0/+3
* Cold feet: suppress builtins for load with reservation/store conditional, use...xleroy2014-08-285-47/+2
* Updatexleroy2014-08-281-1/+2
* Update for 2.4xleroy2014-08-271-23/+37
* Rename __builtin_cntlz to __builtin_clz.xleroy2014-08-2711-6/+25
* More efficient implementations of map, fold, etc.xleroy2014-08-271-164/+109
* More careful detection of inlined builtins. Produces better error messages i...xleroy2014-08-251-0/+1
* Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false.xleroy2014-08-213-5/+10
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-2116-454/+801
* Follow-up to commit 2613xleroy2014-08-201-0/+2
* Add builtins for load with reservation and conditional store.xleroy2014-08-205-1/+39
* Wrong types for strex builtins.xleroy2014-08-201-4/+4
* Better validation of target for ARMxleroy2014-08-201-1/+5
* Obvious typos in commit r2609xleroy2014-08-201-8/+8
* Add some more synchronization builtinsxleroy2014-08-202-1/+39