aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* Inconsistent treatment of "lone" zero-width bit fieldsxleroy2010-09-243-1/+22
| | | | | | | (i.e. not preceded by another bit field). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1516 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bizarre use of struct valuev1.8xleroy2010-09-212-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1513 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* No crash if nonexistent input file.xleroy2010-09-142-2/+3
| | | | | | | Heuristic to choose test data. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1509 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ++ on volatile not supported.xleroy2010-09-041-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1504 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:xleroy2010-09-0210-36/+74
| | | | | | | | | | | | - 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
* Adding __builtin_annotationxleroy2010-09-012-1/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of ↵xleroy2010-09-015-0/+51
| | | | | | reading a small unsigned bitfield git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1496 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:xleroy2010-08-188-7/+87
| | | | | | | | | | | | | | | | | | | | | | - 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
* Bug in cparser/AddCasts.ml.xleroy2010-07-083-1/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1376 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another regressionxleroy2010-05-103-1/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1344 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More struct testsxleroy2010-04-171-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1321 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* __builtin_memcpy, continued.xleroy2010-04-174-0/+88
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1320 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-091-1/+1
| | | | | | | | 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-072-0/+35
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1311 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In cparser/SimplExpr.ml:xleroy2010-04-023-1/+15
| | | | | | | | - 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-013-1/+17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1307 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
* Extra volatile testxleroy2010-03-283-1/+45
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug in multidimensional read-only arraysxleroy2010-03-131-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Handling of volatile accesses through builtin functions.xleroy2010-03-082-0/+68
| | | | | | | | | 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
* Suppressed -fall-extensions option, too dangerous wrt flonglongxleroy2010-03-031-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1275 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
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-0329-0/+384
| | | | 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
* 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
* Backtracking on commit 1220v1.6xleroy2010-01-131-0/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test result more reproduciblexleroy2009-12-162-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1201 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-011-0/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problem with const enum initializersxleroy2009-09-152-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1146 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Stronger constant folding, esp. w.r.t. floatsxleroy2009-08-212-0/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-0/+6
| | | | | | | | | | | | 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
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-111-2/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test for int/float conversionsxleroy2009-01-073-1/+140
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Endianness in testsxleroy2009-01-054-2/+20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Continuation of PowerPC/EABI portxleroy2008-12-312-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@933 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout nouveaux testsxleroy2008-08-0952-0/+8446
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@708 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-311-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update test resultsxleroy2008-07-311-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@704 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Augmenter le temps d'execution par defautxleroy2008-07-252-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@700 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵xleroy2008-04-192-5/+8
| | | | | | dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Amelioration compilation des switchxleroy2008-04-171-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout du test vmachxleroy2008-04-153-1/+219
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@612 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problemes d'alignement des variables globales et a l'interieur de leurs ↵xleroy2007-10-313-3/+53
| | | | | | initialiseurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les ↵xleroy2007-08-282-2/+5
| | | | | | 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
* Rendu le test lists.c plus interessantxleroy2007-08-061-4/+30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 01:32:53 +0000