summaryrefslogtreecommitdiff
path: root/extraction
Commit message (Collapse)AuthorAge
* Use Flocq for floatsGravatar xleroy2012-06-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem branch:Gravatar xleroy2012-05-21
| | | | | | | | | | - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
| | | | | | | | | | | - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsGravatar xleroy2011-10-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added animation of the CompCert C semantics (ccomp -interp)Gravatar xleroy2011-07-28
| | | | | | | | test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).Gravatar xleroy2011-05-08
| | | | | | | | | | Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initializers for global variables: compile-time evaluation of expressions ↵Gravatar xleroy2011-03-12
| | | | | | done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Undesirable optimization of 'print'Gravatar xleroy2011-03-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1601 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.Gravatar xleroy2011-03-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* float->int conversions, continued: weaker axiomatization.Gravatar xleroy2010-10-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1545 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Float.intoffloat and Float.intuoffloat are now partial functions.Gravatar xleroy2010-10-28
| | | | | | | (May fail if float is too big to be converted.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:Gravatar xleroy2010-09-02
| | | | | | | | | | | | - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:Gravatar xleroy2010-08-18
| | | | | | | | | | | | | | | | | | | | | | - 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
* Revised encoding/decoding of floatsGravatar xleroy2010-05-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem and newextcalls branches:Gravatar xleroy2010-03-07
| | | | | | | | | | - 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
* Updated ARM portGravatar xleroy2010-01-25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1232 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC/EABI port: preliminary support for #pragma section andGravatar xleroy2009-11-03
| | | | | | | | | | #pragma use_section. Some clean-ups in Cil2Csyntax. Separate mach-dep parts of extraction/extraction.v into <arch>/extractionMachdep.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified the treatment of the PowerPC small data area; now more specific ↵Gravatar xleroy2009-11-02
| | | | | | to the Diab toolchain. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1165 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for small data area in PowerPC port.Gravatar xleroy2009-11-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated SelectionGravatar xleroy2009-08-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1132 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cil2Csyntax: added goto and labels; added assignment between structsGravatar xleroy2009-08-16
| | | | | | | | | | | | 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
* Use Extraction BlacklistGravatar xleroy2009-07-25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1114 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adapted to work with Coq 8.2-1Gravatar xleroy2009-06-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Various clean-upsGravatar xleroy2009-04-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update creation Configuration.mlGravatar xleroy2009-03-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1022 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive ↵Gravatar xleroy2009-01-29
| | | | | | 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
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30
| | | | | | | | | 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
* Extract Coq lists to Caml lists.Gravatar xleroy2008-12-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@929 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.Gravatar xleroy2008-12-29
| | | | | | | | lib/Integers.v: added more properties for ARM port. lib/Coqlib.v: added more properties for division and powers of 2. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@928 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised back-end so that only 2 integer registers are reserved for reloading.Gravatar xleroy2008-12-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@925 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flag to turn on/off the recognition of fused multiply-add and multiply-subGravatar xleroy2008-07-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ↵Gravatar xleroy2008-05-30
| | | | | | utilisee dans le front-end C. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵Gravatar xleroy2008-04-19
| | | | | | dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJGravatar xleroy2008-04-15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problemes d'alignement des variables globales et a l'interieur de leurs ↵Gravatar xleroy2007-10-31
| | | | | | initialiseurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesGravatar xleroy2007-10-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@443 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGGravatar xleroy2007-10-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJGravatar xleroy2007-10-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@422 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les ↵Gravatar xleroy2007-08-28
| | | | | | expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu MakefilesGravatar xleroy2007-08-06
| | | | 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".Gravatar xleroy2007-08-04
| | | | | | | | | | | | 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 ↵Gravatar xleroy2007-03-02
| | | | | | 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
* Lever la restriction sur les fonctions externes, restriction qui exigeait ↵Gravatar xleroy2006-10-22
| | | | | | que tous les arguments resident en registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ suite ajouts dans Kildall. Compiler en code natif par defautGravatar xleroy2006-09-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@92 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Encore une eta-expansion intempestiveGravatar xleroy2006-09-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@90 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJGravatar xleroy2006-09-08
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@88 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration du front-end CIL developpe par Thomas MoniotGravatar xleroy2006-09-07
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout de dependances dans extraction/MakefileGravatar tristan2006-09-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@80 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu la repartition des sources Coq en sous-repertoiresGravatar xleroy2006-09-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 23:42:39 +0000