aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* MAJ release 2.1v2.1xleroy2013-10-281-10/+25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better prepro options for XCode 5.0xleroy2013-10-281-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Eliminate unreferenced inline functionsxleroy2013-10-281-2/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2353 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revise parsing of character constants for conformance with ISO C 99.xleroy2013-10-252-12/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2352 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix doc comment for loc_arguments.xleroy2013-10-251-6/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2351 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert commit r2349 because it triggers a bug in GNU as.xleroy2013-10-242-18/+29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2350 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use register names under Linux.xleroy2013-10-242-29/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2349 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fine-tuning of the "andimm" case to generate a move rather than an andimm ↵xleroy2013-10-242-2/+13
| | | | | | when possible. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2348 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typing of integer literals: follow C99 rules exactly.xleroy2013-10-211-28/+29
| | | | | | | Comments: make reference to the C99 standard. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2347 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised renumbering of nodes and registers so that main function is not ↵xleroy2013-10-183-48/+114
| | | | | | shifted by 1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cminor parsing and printing (from Andrew Tolmach)xleroy2013-10-167-24/+175
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Warn for volatile accesses to compositesxleroy2013-10-161-0/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2344 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PackedStructs.ml: cleanups and bug-fixesxleroy2013-10-132-15/+17
| | | | | | | Ceval.ml: tolerate non-zero integers with pointer types. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2343 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-0526-428/+538
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Follow-up to commit 2339:xleroy2013-10-051-1/+1
| | | | | | | don't complain about parameter redefinition for unnamed parameters. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2340 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elab:xleroy2013-10-042-29/+34
| | | | | | | | | | | - bad error recovery on bitfield with 'long long' type - check for redefinition of function parameters Bitfields: - when assigning to a bitfield, cast the RHS to "unsigned int" (it matters if the RHS is long long). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Do not use Format for faster printing of RTL, XTL, LTL, Machxleroy2013-09-262-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2338 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Do not use Format for faster printing of RTL, XTL, LTL, Machxleroy2013-09-266-137/+129
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2337 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MacOS X linker option galorexleroy2013-09-261-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2336 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Slightly more efficient conversion positive <-> intxleroy2013-09-261-17/+22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2335 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Small improvements in compilation times for the register allocation pass.xleroy2013-09-206-22/+86
| | | | | | | Maps.v: add a PTree.fold1 operation that doesn't maintain the key. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-1420-107/+374
| | | | | | | | | are necessary, only two parameters (default_pl and choose_binop_pl). SelectDiv: optimize FP division by a power of 2. ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Change the way arguments to __builtin_annot are converted. Use the same ↵xleroy2013-09-141-2/+6
| | | | | | conventions as other variadic functions such as printf(). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2325 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Oops, wrong commit of generated files.xleroy2013-08-242-758/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2311 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to add these two files.xleroy2013-08-242-0/+758
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2310 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplify LPMap by smashing bottoms.xleroy2013-08-122-145/+48
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2306 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Change interface of Kildall solvers to avoid precomputing the map pc -> list ↵xleroy2013-08-1220-237/+288
| | | | | | of successors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add test for NaNsxleroy2013-08-022-4/+95
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2304 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Flocq version 2.2.0.xleroy2013-08-0238-364/+2378
| | | | | | | More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Alternate characterization of alignment constraints in memory injection, ↵xleroy2013-07-311-107/+108
| | | | | | which works better than the old one for the VST project. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update cchecklink w/ new Asm instructions Pmulh*xleroy2013-07-292-0/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2301 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-2936-182/+2663
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add another expansion of shrx in terms of shifts and adds (from Hacker's ↵xleroy2013-07-281-42/+72
| | | | | | Delight). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2299 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More properties about subtraction and borrow.xleroy2013-07-151-18/+59
| | | | 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.xleroy2013-07-139-327/+655
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of int->float conversions:xleroy2013-07-085-17/+106
| | | | | | | | | | - 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.xleroy2013-07-081-1/+4
| | | | 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.xleroy2013-07-072-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2292 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bad printing of alignment on 'comm' symbols.xleroy2013-07-073-5/+9
| | | | 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 twoxleroy2013-07-0317-20/+475
| | | | | | | | 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.xleroy2013-07-032-25/+502
| | | | 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 IA32xleroy2013-07-035-70/+220
| | | | | | | | 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.0v2.0xleroy2013-06-213-4/+4
| | | | 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 ↵xleroy2013-06-215-18/+58
| | | | | | "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.xleroy2013-06-201-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2284 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates in preparation for release 2.00xleroy2013-06-192-52/+20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* One more copyright header update.xleroy2013-06-171-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updating LICENSE and license headers, continued.xleroy2013-06-172-0/+5
| | | | 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.xleroy2013-06-177-402/+55
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in commentxleroy2013-06-171-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2279 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-11 18:47:49 +0000