aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Last updates for release 1.5.v1.5xleroy2009-08-283-20/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1142 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for release 1.5xleroy2009-08-272-2/+33
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1141 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove "-ccopt -g" options: not really useful and causing problems with ↵xleroy2009-08-271-2/+2
| | | | | | flexdll in the Win32/mingw port of Caml. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-265-126/+266
| | | | | | | | | | nodes a la Appel and George. Maps: in PTree.combine, compress useless subtrees. Lattice: more efficient implementation of LPMap. Makefile: build profiling version git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in docxleroy2009-08-261-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1138 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Stronger constant folding, esp. w.r.t. floatsxleroy2009-08-213-40/+165
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In generated Cminor functions, make sure local variables includexleroy2009-08-202-23/+100
| | | | | | | | all x used as destination of a call [x = f(args)]. This wasn't true before if x was a global C#minor variable. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1136 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Build bytecode version with debug symbols.xleroy2009-08-201-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated Selectionxleroy2009-08-181-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1132 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Declaration of use_fused_mul, unused in this port but needed for extraction ↵xleroy2009-08-181-0/+4
| | | | | | (I think) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1131 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to add some filesxleroy2009-08-182-0/+717
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1130 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* No '\n' in Coq strings...xleroy2009-08-183-4/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-183-22/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo docxleroy2009-08-171-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactoring of Constprop and Constpropproof into a machine-dependent part ↵xleroy2009-08-178-1327/+776
| | | | | | and a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + ↵xleroy2009-08-178-1548/+325
| | | | | | a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-1624-523/+608
| | | | | | | | | | | | Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-1610-657/+916
| | | | | | | | | | | | | | and reactive divergence. As a consequence: - Removed the Enilinf constructor from traceinf (values of traceinf type are always infinite traces). - Traces are now uniquely defined. - Adapted proofs big step -> small step for Clight and Cminor accordingly. - Strengthened results in driver/Complements accordingly. - Added common/Determinism to collect generic results about deterministic semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Unionfind data structure, used in new implementation of backend/Tunnelingxleroy2009-08-161-0/+702
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1122 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update spill costs when coalescingxleroy2009-08-161-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1121 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added 'going wrong' behaviorsxleroy2009-08-0526-273/+449
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Transition semantics for Clight and Csharpminorxleroy2009-08-0311-2365/+3013
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Extraction Blacklistxleroy2009-07-254-21/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1114 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJxleroy2009-07-151-11/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1107 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* message macosx en accord avec configureblazy2009-06-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1079 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-0571-852/+795
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Various clean-upsv1.4xleroy2009-04-179-75/+61
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Configuration.systemxleroy2009-03-291-28/+38
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1023 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update creation Configuration.mlxleroy2009-03-291-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1022 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cil.patch dir now uselessxleroy2009-03-290-0/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1021 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up configure script.xleroy2009-03-29296-1356/+82317
| | | | | | | | Distribution of CIL as an expanded source tree with changes applied (instead of original .tar.gz + patches to be applied at config time). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug with overflow in line numbersxleroy2009-03-291-0/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1019 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Honor "static" modifier on C globals.xleroy2009-03-283-32/+104
| | | | | | | | Put "const" globals in read-only section. Revised printing of rlwinm instruction. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1018 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatexleroy2009-03-261-0/+25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1016 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added tail call optimization passxleroy2009-03-269-9/+889
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1015 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize redundant casts after memory loadsxleroy2009-02-272-0/+58
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1002 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* New linearization heuristicxleroy2009-02-271-32/+72
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1001 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* make install: ./ccomp au lieu de ../ccompblazy2009-02-271-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1000 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x ↵xleroy2009-02-2610-39/+156
| | | | | | >= 0' and 'x < 0'. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@999 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive ↵xleroy2009-01-2911-34/+25
| | | | | | file systems. Replaced CList by CoqList and likewise for CString and CInt. Removed useless references to CList in hand-written Caml code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-118-30/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Added alignment constraints to memory loads and stores.xleroy2009-01-1167-1488/+719
| | | | | | | | | | | - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed unary minusxleroy2009-01-071-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@944 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test for int/float conversionsxleroy2009-01-073-1/+140
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatesxleroy2009-01-053-33/+58
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Endianness in testsxleroy2009-01-054-2/+20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-044-8/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@938 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Some cleanupsxleroy2009-01-021-1/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@937 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong dependenciesxleroy2009-01-021-4/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@936 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Continuation of ARM port.xleroy2009-01-017-38/+1226
| | | | | | | Cleaned up Makefile and SVN properties. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@935 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-03 04:28:10 +0000