summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* More properties about subtraction and borrow.Gravatar xleroy2013-07-15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More accurate model of condition register flags for ARM and IA32.Gravatar xleroy2013-07-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of int->float conversions:Gravatar xleroy2013-07-08
| | | | | | | | | | - introduce Float.floatofint{,u} and use it in the semantics of C - prove that it is equivalent to int->double conversion followed by double->float rounding, and use this fact to justify code generation in Cshmgen. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -no-runtime-lib.Gravatar xleroy2013-07-08
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2293 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compile in debug mode and activate stack backtraces.Gravatar xleroy2013-07-07
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2292 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bad printing of alignment on 'comm' symbols.Gravatar xleroy2013-07-07
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat casts int64 -> float32 as primitive operations instead of twoGravatar xleroy2013-07-03
| | | | | | | | casts int64 -> float64 -> float32. The latter causes double rounding errors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Follow-up to commit 2288: add test for special case of long division.Gravatar xleroy2013-07-03
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2289 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc: faster implementation of long division modeled on that for IA32Gravatar xleroy2013-07-03
| | | | | | | | test: add one test (2^64-1) / (2^32+3) to exercise a special case of this long division. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2288 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Version 2.00 -> version 2.0Gravatar xleroy2013-06-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognize attribute((packed)) after a "struct {...}" and not just between ↵Gravatar xleroy2013-06-21
| | | | | | "struct" and "{", for compatibility with GCC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Missing case for EF_inline_asm.Gravatar xleroy2013-06-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2284 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates in preparation for release 2.00Gravatar xleroy2013-06-19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* One more copyright header update.Gravatar xleroy2013-06-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updating LICENSE and license headers, continued.Gravatar xleroy2013-06-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2281 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update LICENSE file and headers for dual-licensed files.Gravatar xleroy2013-06-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in commentGravatar xleroy2013-06-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2279 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update version numberGravatar xleroy2013-06-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2278 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for release 2.00Gravatar xleroy2013-06-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2277 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:Gravatar xleroy2013-06-16
| | | | | | | | | | | | | | - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More precise and faster recovery of function name from function or fundef value.Gravatar xleroy2013-06-08
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix compilation of runtime system.Gravatar xleroy2013-05-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2263 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Hunting stack overflows again:Gravatar xleroy2013-05-27
| | | | | | | | PrintLTL: List.map -> List.rev_map IRC: @ -> List.rev_append + don't maintain "extra" lists on precolored nodes. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2262 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc: tentative support for Diab debug infoGravatar xleroy2013-05-20
| | | | | | | arm, ia32: reset table of file names at each run git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2261 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the float32 branch: Gravatar xleroy2013-05-19
| | | | | | | | - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Prettier outputGravatar xleroy2013-05-19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2258 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Issue with simplification of nested ?: expressions of different types.Gravatar xleroy2013-05-19
| | | | | | | | (Ill-typed Clight/Cminor/RTL code was generated due to incorrect reuse of destination temporary.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2257 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -fno-tailcalls to turn off tailcall elimination (causes problem ↵Gravatar xleroy2013-05-17
| | | | | | | | | with some static analysis tools). */PrintAsm.ml: don't cfa_adjust at Pfreeframe, as more code from the function can appear after (in case of tailcalls). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2256 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update PowerPC portGravatar xleroy2013-05-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2255 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update ARM port.Gravatar xleroy2013-05-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for debugging info (-g).Gravatar xleroy2013-05-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* "->" can be applied to an array, not just a pointer.Gravatar xleroy2013-05-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2251 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MacOS: try to add link option -Wl,-no-pie when needed e.g. 10.8 and up.Gravatar xleroy2013-05-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2249 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support __attribute__(ident) where ident is not bound. Useful for GCC ↵Gravatar xleroy2013-05-13
| | | | | | compatibility in general and MacOS 10.8 standard includes in particular. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2248 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Missing case: initialization of a global variable of type _Bool.Gravatar xleroy2013-05-08
| | | | | | | Added corresponding test case. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2242 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add interferences at function entry with destroyed_at_function_entry.Gravatar xleroy2013-05-08
| | | | | | | Improve dead code elimination for Xparmove. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2241 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised semantics and compilation of 2-argument C operators to better match Gravatar xleroy2013-05-06
| | | | | | | | "the usual binary conversions" and be more robust towards future extensions e.g. with 32-bit float values. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2239 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactoring: move definition of chunk_of_type to AST.v.Gravatar xleroy2013-05-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2238 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Syntax errorsGravatar xleroy2013-05-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2237 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong pseudo-instrGravatar xleroy2013-05-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2236 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for in64 -> float conversions w/ correct rounding.Gravatar xleroy2013-05-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ia32/i64_dtou: wrong play on rounding modeGravatar xleroy2013-05-05
| | | | | | | | | arm, powerpc: expand shifts inline in dtos and dtou arm: branchless code for shl and shr test: more tests for double -> long long conversions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2234 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extend CSE of loads following stores to chunks Mint64 and Mfloat64al32.Gravatar xleroy2013-05-02
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2231 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Stack-align to 8 arguments of Tfloat and Tlong types, as per the SVR4 ABI ↵Gravatar xleroy2013-05-02
| | | | | | and the EABI. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2230 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clean up 'make clean'Gravatar xleroy2013-05-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2229 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use "-as" to put CompCert modules in a compcert.xxx namespace.Gravatar xleroy2013-05-01
| | | | | | | | Simplified the scripts "coq" and "pg". Updated deps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Oops, removed a crucial declaration for Allocation.Gravatar xleroy2013-05-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2227 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coq-defined equality functions for Allocation. (continued)Gravatar xleroy2013-05-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2226 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coq-defined equality functions for Allocation.Gravatar xleroy2013-05-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2225 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removing modules now unusedGravatar xleroy2013-05-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2224 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 08:17:55 +0000