aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* Updates for IA32-Cygwin.xleroy2010-09-081-3/+11
| | | | | | | | cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified stdlib wrapper; use it only under MacOS Xxleroy2010-09-041-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-181-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:xleroy2010-08-181-2/+4
| | | | | | | | | | | | | | | | | | | | | | - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inlined built-ins.xleroy2010-06-291-2/+2
| | | | | | | | | | | | | AST: add ef_inline flag to external functions. Selection: recognize calls to inlined built-ins and inline them as Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm: adapted expansion of builtins. C2Clight: adapted detection of builtins. Conventions: refactored in a machine-independent part (backend/Conventions) and a machine-dependent part (ARCH/SYS/Conventions1). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merging the Princeton implementation of the memory model. Separate axioms ↵xleroy2010-06-281-1/+1
| | | | | | in file lib/Axioms.v. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaner generation of .dependxleroy2010-03-301-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* New HTML documentation generatorxleroy2010-03-091-15/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-2/+2
| | | | | | | | | | - Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppressed Init_pointer, now useless. Improved printing of strings in ↵xleroy2010-03-031-0/+1
| | | | | | generated .s git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1274 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-9/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-261-1/+5
| | | | | | | | | | 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
* 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
* Refactoring of Constprop and Constpropproof into a machine-dependent part ↵xleroy2009-08-171-1/+1
| | | | | | 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-171-1/+1
| | | | | | a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-1/+1
| | | | | | | | | | | | | | 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
* Added 'going wrong' behaviorsxleroy2009-08-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Various clean-upsv1.4xleroy2009-04-171-10/+27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added tail call optimization passxleroy2009-03-261-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1015 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
* Updatesxleroy2009-01-051-2/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@940 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-011-7/+16
| | | | | | | Cleaned up Makefile and SVN properties. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@935 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-19/+40
| | | | | | | | | Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu removeproofxleroy2008-03-191-1/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout de common/Complements.vxleroy2007-08-261-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefilesxleroy2007-08-061-8/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-16/+24
| | | | | | | | | | | | En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation ↵xleroy2007-03-021-1/+1
| | | | | | de Lattice pour utiliser une notion d'egalite possiblement differente de =. Adaptation de Kildall et de ses utilisateurs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-111-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration du front-end CIL developpe par Thomas Moniotxleroy2006-09-071-0/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-7/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche "traces":xleroy2006-09-041-7/+11
| | | | | | | | | | | | | - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initial import of compcertxleroy2006-02-091-0/+75
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 01:41:49 +0000