aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge of the newmem and newextcalls branches:xleroy2010-03-0730-842/+951
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-5/+7
* Backtracking on commit 1220v1.6xleroy2010-01-1341-23329/+14
* ajout branche allocation de registresblazy2010-01-0841-14/+23329
* MAJ extraction after changes in Integersxleroy2009-12-161-1/+1
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-192-6/+6
* More realistic treatment of jump tables: show the absence of overflow when ac...xleroy2009-11-106-3/+13
* Added support for jump tables in back end.xleroy2009-11-1040-88/+380
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-261-60/+132
* Forgot to add some filesxleroy2009-08-182-0/+717
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-181-0/+11
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-172-0/+680
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-171-0/+122
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-1614-349/+346
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-162-26/+34
* Update spill costs when coalescingxleroy2009-08-161-2/+3
* Added 'going wrong' behaviorsxleroy2009-08-0511-165/+167
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-23/+17
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-0526-229/+168
* Added tail call optimization passxleroy2009-03-263-6/+847
* New linearization heuristicxleroy2009-02-271-32/+72
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-294-10/+6
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-115-24/+0
* - Added alignment constraints to memory loads and stores.xleroy2009-01-1138-537/+137
* Fixed unary minusxleroy2009-01-071-1/+1
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-042-4/+0
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-3032-11274/+2075
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-298-44/+49
* Revised back-end so that only 2 integer registers are reserved for reloading.xleroy2008-12-2119-402/+780
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-312-20/+29
* MAJ documentationxleroy2008-07-276-361/+110
* Simplification de la semantique de LTL et LTLin. Les details lies aux conven...xleroy2008-07-258-523/+538
* Fusion partielle de la branche contsem: xleroy2008-07-088-1732/+1652
* Nettoyage du traitement des signatures au return dans LTL et LTLinxleroy2008-07-076-107/+96
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...xleroy2008-05-303-52/+77
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-308-4/+55
* Revu le traitement de la 'red zone' en bas de la pilexleroy2008-04-128-58/+65
* Revu gestion retaddr et link dans Stackingxleroy2008-04-1217-934/+1032
* Meilleure selection pour if ((a && b) != 0), etcxleroy2008-03-272-27/+277
* Nettoyages docxleroy2008-03-192-15/+6
* Ajout license, README, copyright noticesxleroy2008-01-2755-0/+663
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-313-79/+59
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGxleroy2007-10-273-158/+257
* Typo dans le pseudocode en commentairexleroy2007-10-171-1/+1
* Utilisation d'une monade avec types dependants pour garder trace des propriet...xleroy2007-10-173-556/+461
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-287-1407/+1739
* Ajout de common/Complements.vxleroy2007-08-261-0/+3
* Documentationxleroy2007-08-056-119/+126
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-0455-10999/+12921
* Importer OrderedPositive depuis Ordered.vxleroy2007-03-051-30/+1
generated by cgit (git 2.34.1) at 2024-06-02 16:55:22 +0000