summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Preliminary support for small data area in PowerPC port.Gravatar xleroy2009-11-01
* Support Clight initializers of the form "int * x = &y;".Gravatar xleroy2009-11-01
* Storing of single floats: must insert frsp instruction before store. (Tempor...Gravatar xleroy2009-10-30
* Problem with MacOS X 10.6Gravatar xleroy2009-10-25
* Problem with const enum initializersGravatar xleroy2009-09-15
* Updated for 1.5Gravatar xleroy2009-09-15
* Last updates for release 1.5.Gravatar xleroy2009-08-28
* Updated for release 1.5Gravatar xleroy2009-08-27
* Remove "-ccopt -g" options: not really useful and causing problems with flexd...Gravatar xleroy2009-08-27
* Coloringaux: make identifiers unique; special treatment of precolored Gravatar xleroy2009-08-26
* Typo in docGravatar xleroy2009-08-26
* Stronger constant folding, esp. w.r.t. floatsGravatar xleroy2009-08-21
* In generated Cminor functions, make sure local variables includeGravatar xleroy2009-08-20
* Build bytecode version with debug symbols.Gravatar xleroy2009-08-20
* Updated SelectionGravatar xleroy2009-08-18
* Declaration of use_fused_mul, unused in this port but needed for extraction (...Gravatar xleroy2009-08-18
* Forgot to add some filesGravatar xleroy2009-08-18
* No '\n' in Coq strings...Gravatar xleroy2009-08-18
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.Gravatar xleroy2009-08-18
* Typo docGravatar xleroy2009-08-17
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...Gravatar xleroy2009-08-17
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...Gravatar xleroy2009-08-17
* Cil2Csyntax: added goto and labels; added assignment between structsGravatar xleroy2009-08-16
* Distinguish two kinds of nonterminating behaviors: silent divergenceGravatar xleroy2009-08-16
* Unionfind data structure, used in new implementation of backend/TunnelingGravatar xleroy2009-08-16
* Update spill costs when coalescingGravatar xleroy2009-08-16
* Added 'going wrong' behaviorsGravatar xleroy2009-08-05
* Transition semantics for Clight and CsharpminorGravatar xleroy2009-08-03
* Use Extraction BlacklistGravatar xleroy2009-07-25
* MAJGravatar xleroy2009-07-15
* message macosx en accord avec configureGravatar blazy2009-06-05
* Adapted to work with Coq 8.2-1Gravatar xleroy2009-06-05
* Various clean-upsGravatar xleroy2009-04-17
* Use Configuration.systemGravatar xleroy2009-03-29
* Update creation Configuration.mlGravatar xleroy2009-03-29
* cil.patch dir now uselessGravatar xleroy2009-03-29
* Cleaned up configure script.Gravatar xleroy2009-03-29
* Bug with overflow in line numbersGravatar xleroy2009-03-29
* Honor "static" modifier on C globals.Gravatar xleroy2009-03-28
* UpdateGravatar xleroy2009-03-26
* Added tail call optimization passGravatar xleroy2009-03-26
* Optimize redundant casts after memory loadsGravatar xleroy2009-02-27
* New linearization heuristicGravatar xleroy2009-02-27
* make install: ./ccomp au lieu de ../ccompGravatar blazy2009-02-27
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...Gravatar xleroy2009-02-26
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...Gravatar xleroy2009-01-29
* Elimination of "alloc" instruction in Caml files and test files.Gravatar xleroy2009-01-11
* - Added alignment constraints to memory loads and stores.Gravatar xleroy2009-01-11
* Fixed unary minusGravatar xleroy2009-01-07
* Test for int/float conversionsGravatar xleroy2009-01-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 12:45:05 +0000