summaryrefslogtreecommitdiff
path: root/driver/Driver.ml
Commit message (Expand)AuthorAge
* Merge of the newmem branch:Gravatar xleroy2012-05-21
* checklink: first import of Valentin Robert's validator for asm and linkGravatar xleroy2012-03-28
* Option -randvol to expose randomization of volatiles in Interp.mlGravatar xleroy2012-03-12
* Merge of Andrew Tolmach's HASP-related changesGravatar xleroy2012-03-09
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsGravatar xleroy2012-03-07
* Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt>Gravatar xleroy2012-02-29
* Merge of the "volatile" branch:Gravatar xleroy2012-02-04
* Interp: accommodate "int main(int, char **)".Gravatar xleroy2011-10-19
* Corrected initialization of char arrays by string literals.Gravatar xleroy2011-10-17
* Presimplification SimplVolatile: cleaned up and integrated.Gravatar xleroy2011-08-18
* Added animation of the CompCert C semantics (ccomp -interp)Gravatar xleroy2011-07-28
* cparser: support for attributes over struct and union.Gravatar xleroy2011-05-12
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).Gravatar xleroy2011-05-08
* Revised signed/unsigned char handling.Gravatar xleroy2011-03-10
* Treat "char" as unsigned OR signed depending on the configuration.Gravatar xleroy2011-03-09
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...Gravatar xleroy2010-10-27
* Simplified stdlib wrapper; use it only under MacOS XGravatar xleroy2010-09-04
* Merge of the reuse-temps branch:Gravatar xleroy2010-09-02
* Renamed C2Clight into C2CGravatar xleroy2010-08-18
* Merge of branches/full-expr-4:Gravatar xleroy2010-08-18
* Cleaned up handling of linker sections.Gravatar xleroy2010-05-08
* Options -I -D -U with a spaceGravatar xleroy2010-03-30
* Handling of volatile accesses through builtin functions.Gravatar xleroy2010-03-08
* Handling of builtins, continued.Gravatar xleroy2010-03-07
* Suppressed -fall-extensions option, too dangerous wrt flonglongGravatar xleroy2010-03-03
* Switching to the new C parser/elaborator/simplifierGravatar xleroy2010-03-03
* Revised handling of #pragma section and small data areasGravatar xleroy2010-01-27
* PowerPC/EABI port: preliminary support for #pragma section andGravatar xleroy2009-11-03
* Simplified the treatment of the PowerPC small data area; now more specific to...Gravatar xleroy2009-11-02
* Preliminary support for small data area in PowerPC port.Gravatar xleroy2009-11-01
* No '\n' in Coq strings...Gravatar xleroy2009-08-18
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 00:07:29 +0000