aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Remove __i64_{neg,add,sub,mul}, now handled directly by the compiler.xleroy2013-04-204-171/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2204 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added FFTW benchmark provided by Guillaume Melquiondxleroy2013-04-203-2/+107
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2203 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Tests "floats" and "floats-basics" moved from test/c to test/regressionxleroy2013-04-207-21/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2202 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp.ml: support printf of long longxleroy2013-04-206-60/+4197
| | | | | | | test/regression: add test "int32"; update test "int64" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2201 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-20166-10626/+20598
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated issues with coqchk. See PR#3026 on the Coq bug tracker.xleroy2013-04-141-6/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2189 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* List.iteri not in OCaml < 4.00, better not use it.xleroy2013-04-081-2/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatedxleroy2013-03-262-18/+23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2164 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Error when calling un-prototyped function.xleroy2013-03-251-6/+8
| | | | | | | Removed warning "un-prototyped function type", fires too often. The important thing is to mark errors when declaring and calling unproto fns. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2160 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better locations for error messages relative to type specifiers.xleroy2013-03-251-14/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2159 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Watch out for behaviors exponential in the nesting of struct/union types. xleroy2013-03-236-66/+78
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* RTLtyping: now performed entirely in Coq, no need for an external Caml ↵xleroy2013-03-223-374/+713
| | | | | | oracle + a validator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2157 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update clightgen to changes in Camlcoq and in AST.xleroy2013-03-202-15/+33
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2156 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Diab asm syntax issuexleroy2013-03-201-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2155 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ↵xleroy2013-03-182-3/+13
| | | | | | limitation in the a3 analyzers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2154 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove the C primitives for unsigned long long arithmetic, replacedxleroy2013-03-184-53/+25
| | | | | | | by pure OCaml code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2153 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive CSE across Ibuiltin.xleroy2013-03-173-7/+36
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2152 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted changes to reduce stack and heap requirements when compiling very ↵xleroy2013-03-1635-237/+534
| | | | | | big functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Machsem: no longer useful.xleroy2013-03-141-259/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2150 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bind some local defs with Let, makes extracted code cleanerv1.13xleroy2013-03-121-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2148 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Maps: revised TREE interface; added mucho derived properties and operations ↵xleroy2013-03-122-63/+256
| | | | | | | | | in Tree_Properties. Lattice: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2147 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppress int64_unsigned_to_float, now unused.xleroy2013-03-112-7/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2146 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More updates for 1.13xleroy2013-03-111-2/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2145 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed parsing of hex float literals 0xNNNpMMM.xleroy2013-03-115-4/+81
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2144 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for version 1.13xleroy2013-03-112-11/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2143 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updating doc for 1.13xleroy2013-03-111-8/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2142 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Useless Importxleroy2013-03-101-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2141 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-1029-120/+133
| | | | | | | | for no good reason. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-0910-215/+260
| | | | | | | | submodules. (Extraction does not remove them, then.) common/Switch: replaced use of FMaps by our own Maps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improving the performance of exhaustive exploration (mode -all):xleroy2013-03-091-18/+112
| | | | | | | | - Re-share states even at different times - Faster comparison between states, giving priority to the mem nextblock git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2138 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-047-815/+593
| | | | | | | ARM: slightly shorter code generated for indirect memory accesses. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-037-857/+757
| | | | | | | | trick prevents a future mapping of the Mach/Asm call stack as a single block. IA32 is fixed, PowerPC and ARM remains to be done. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2136 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates to follow recent changes in PrintAsm.mlxleroy2013-03-011-14/+43
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Some builtins were renamed, updatingxleroy2013-03-011-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2134 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug in Pbtblxleroy2013-03-011-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2133 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* No longer a dependency on Machtypingxleroy2013-03-012-2/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2132 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix 'interp' entryxleroy2013-03-011-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2131 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Testing dense switchesxleroy2013-03-013-1/+62
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2130 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-0126-7039/+4809
| | | | | | | | | | - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-249-90/+93
| | | | | | | ARM: add support for builtin_volatile_{read,write}_global, after all. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constant propagation within __builtin_annot.xleroy2013-02-2415-124/+250
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pointers one pastxleroy2013-02-1521-324/+565
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated PowerPC port to new integers.xleroy2013-02-128-29/+59
| | | | | | | Added options -falign-branch-targets and -falign-cond-branches (experimental). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2113 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Be more like gcc in the way we display or not the usage message.xleroy2013-02-121-8/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot theorem "sign_ext_narrow".xleroy2013-02-121-0/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-1011-1450/+1733
| | | | | | | | bit-level operations provided by ZArith in Coq 8.4. Other modules: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Some more properties. Refactored some proofs.xleroy2013-02-041-21/+107
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2109 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in compare_mem causing merging of different states.xleroy2013-02-021-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2108 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Errors for excessively large global variables or stack frames.xleroy2013-02-026-14/+17
| | | | | | | test/: update Makefiles so that "all" is the default target. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2107 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Camlcoq.ml: bug in conversion Z to stringv1.12.1xleroy2013-01-292-4/+4
| | | | | | | PrintClight: forgot "$" prefix on temporary names git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2102 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-03 05:37:45 +0000