aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Update for 1.7.1v1.7.1xleroy2010-04-131-0/+17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1317 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC: xleroy2010-04-103-3/+32
| | | | | | | | | - added __builtin_trap() - generate .size and .type directives - use natural alignment for variables git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1315 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloring: allow to exclude user-specified registers from allocation.xleroy2010-04-105-28/+131
| | | | | | | CPragmas (PPC/EABI only): add #pragma reserve_register git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1314 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test bit field of size 32xleroy2010-04-093-1/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1313 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.xleroy2010-04-0910-59/+53
| | | | | | | | Algorithmic efficiency: in cparser/, precompute sizeof and alignof of composites. Code cleanup: introduced Cutil.composite_info_{def,decl} git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1312 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Static initialization of structs with bitfieldsxleroy2010-04-073-1/+109
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1311 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong type for __builtin_volatile_*_int32xleroy2010-04-021-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1309 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In cparser/SimplExpr.ml:xleroy2010-04-024-12/+30
| | | | | | | | - wrong simplification of && and || in the Set case - generated nicer code for && and || in the Eval case git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1308 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/AddCasts.ml: forgot to materialize cast at return statement.xleroy2010-04-014-13/+29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1307 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for release 1.7v1.7xleroy2010-03-302-9/+64
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 1.7xleroy2010-03-302-2/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1304 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Determine endianness at run-timexleroy2010-03-301-21/+23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Options -I -D -U with a spacexleroy2010-03-301-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated Linux conventionsxleroy2010-03-301-3/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1301 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaner generation of .dependxleroy2010-03-302-69/+65
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Include targets of preference edges in all_interf_regs. Not needed for ↵xleroy2010-03-301-6/+8
| | | | | | correctness, but this way temporaries that have preferences but no interferences do not fall in the default case of Coloring.alloc_of_coloring. This used to create uncoalesced moves esp. on Arm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1299 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pretty stringsxleroy2010-03-291-3/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extra volatile testxleroy2010-03-283-1/+45
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More resistant proofxleroy2010-03-281-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1296 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Prettier printing of configurationxleroy2010-03-281-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1295 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM asm printerxleroy2010-03-281-4/+67
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typoxleroy2010-03-281-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1293 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Emit a few comments to help reading the generated asmxleroy2010-03-281-10/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1292 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updating ARM portxleroy2010-03-284-61/+41
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug in multidimensional read-only arraysxleroy2010-03-132-7/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* TeX and HTML escapesxleroy2010-03-121-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1289 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Copyright noticexleroy2010-03-121-0/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1288 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Restored the big-step semantics for Cminorxleroy2010-03-111-125/+125
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1287 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* New HTML documentation generatorxleroy2010-03-095-50/+570
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Handling of volatile accesses through builtin functions.xleroy2010-03-089-60/+412
| | | | | | | | | Added support for processor-specific builtin functions. Added some PowerPC instructions as builtins. Updated #pragma section handling. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Handling of builtins, continued.xleroy2010-03-077-51/+57
| | | | | | | PrintCsyntax, PrintAsm: improve printing of float literals. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1284 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised treatment of builtinsxleroy2010-03-0710-244/+300
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem and newextcalls branches:xleroy2010-03-0776-6210/+10378
| | | | | | | | | | - 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 -fall-extensions option, too dangerous wrt flonglongxleroy2010-03-033-12/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1275 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppressed Init_pointer, now useless. Improved printing of strings in ↵xleroy2010-03-036-47/+25
| | | | | | generated .s git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1274 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Detect struct assignment. Silence some warningsxleroy2010-03-031-3/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1273 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for 'inline' modifierxleroy2010-03-034-20/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1272 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated raytracer test. Added SPASS test.xleroy2010-03-03129-159/+83911
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Getting rid of CILxleroy2010-03-03280-83521/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-0390-105/+11165
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Protoizedxleroy2010-03-021-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1268 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Protoizedxleroy2010-03-021-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1267 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Function types didn't always degrade to pointers like they should. ↵xleroy2010-03-024-23/+26
| | | | | | Introduced and used Csyntax.typeconv to address this issue and reduce the number of cases in the classify functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1266 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong rlwinm generated for 'x mod 1'xleroy2010-03-022-111/+110
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1265 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in Makefilexleroy2010-02-171-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganization test directoryxleroy2010-02-17235-15573/+50
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* 3 more benchmarksxleroy2010-02-177-1/+863
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1252 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Moved test harness C files herexleroy2010-02-1714-1/+1649
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1251 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Existence of behaviorsxleroy2010-01-312-15/+176
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1237 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of #pragma section and small data areasxleroy2010-01-275-153/+239
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-12 03:45:32 +0000