aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* some more exampleDavid Monniaux2019-01-195-1/+128
|
* use a prime in PRNGDavid Monniaux2019-01-193-3/+3
|
* quicksortDavid Monniaux2019-01-196-27/+138
|
* fixes in MakefileDavid Monniaux2019-01-191-7/+1
|
* fix MakefileDavid Monniaux2019-01-181-2/+2
|
* more on matricesDavid Monniaux2019-01-183-5/+68
|
* loop transformationDavid Monniaux2019-01-183-2/+50
|
* adjust pathDavid Monniaux2019-01-181-1/+1
|
* moved to subdirectoryDavid Monniaux2019-01-184-1/+1
|
* some unrollingDavid Monniaux2019-01-184-3/+47
|
* fix free() bugDavid Monniaux2019-01-181-0/+2
|
* fourth versionDavid Monniaux2019-01-183-2/+38
|
* some better experiments...David Monniaux2019-01-181-2/+5
|
* clearer filenamesDavid Monniaux2019-01-181-13/+24
|
* bugfixDavid Monniaux2019-01-171-1/+1
|
* various matrix multiplication proceduresDavid Monniaux2019-01-173-4/+38
|
* show cycle countsDavid Monniaux2019-01-171-2/+44
|
* so that we can compare gcc and ccomp .sDavid Monniaux2019-01-171-3/+6
|
* for testing postpassDavid Monniaux2019-01-174-35/+64
|
* test (does not compile yet)David Monniaux2019-01-172-0/+115
|
* Fixed the forvar testCyril SIX2019-01-172-3/+13
|
* Added the use of two va_list in a va_arg testCyril SIX2018-12-111-3/+9
|
* In va_arg tests, 2nd argument of va_start is now correctCyril SIX2018-12-112-9/+9
|
* Fixed div64 and mod64Cyril SIX2018-12-112-20/+25
|
* Added printf to the unitary tests for instructionsCyril SIX2018-12-072-27/+29
|
* Added a printf wrapper in test/mppa/libCyril SIX2018-12-074-0/+160
|
* Finished implementation of va_arg + testing doneCyril SIX2018-11-302-4/+4
|
* Wrote some tests on va_arg, need to implement __compcert_va_int32 & cieCyril SIX2018-11-282-7/+467
|
* Added a jobs parameter to the test scriptsCyril SIX2018-11-284-7/+13
|
* Added GCC-compcert call test with a very high register pressureCyril SIX2018-11-285-9/+212
|
* Added tests where GCC calls CompCert functionsCyril SIX2018-11-275-9/+26
|
* Interoperability tests passed (no va_arg yet)Cyril SIX2018-11-2314-0/+355
|
* Fixed andd test not consistent with the restCyril SIX2018-11-231-1/+1
|
* Mise à jour vis à vis de CompCert 3.4Cyril SIX2018-11-211-2/+16
|
* Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-2117-65/+1166
|\ | | | | | | | | Conflicts: .gitignore
| * Attach _Alignas to names and refactor _Alignas checks (#133)Bernhard Schommer2018-09-102-6/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Refactor common code of alignas. Instead of working on attributes the function now works directly on the type since the check always performed an extraction of attributes from a type. Bug 23393 * Attach _Alignas to the name. Bug 23393 * Attach "aligned" attributes to names So that __attribute((aligned(N))) remains consistent with _Alignas(N). gcc and clang apply "aligned" attributes to names, with a special case for typedefs: typedef __attribute((aligned(16))) int int_al_16; int_al_16 * p; __attribute((aligned(16))) int * q; For gcc, p is naturally-aligned pointer to 16-aligned int and q is 16-aligned pointer to naturally-aligned int. For CompCert with this commit, both p and q are 16-aligned pointers to naturally-aligned int. * Resurrect the alignment test involving typedef The test was removed because it involved an _Alignas in a typedef, which is no longer supported. However the same effect can be achieved with an "aligned" attribute, which is still supported in typedef.
| * Improve execution of regression testsXavier Leroy2018-08-244-16/+45
| | | | | | | | | | | | - Make it possible to skip tests on some platforms - Make it possible to expect a failure (typically: of the reference interpreter) - Stop on error
| * Harden the extasm.c test, continuedXavier Leroy2018-08-202-5/+5
| | | | | | | | | | Follow-up to b9a6a50. clang is not happy with COMPCERT_MODEL=32sse2 ("bad suffix on integer"), so use MODEL_32sse2 and ARCH_x86 instead.
| * Harden the extasm.c testXavier Leroy2018-08-202-2/+7
| | | | | | | | | | | | | | Pass more info from CompCert's configuration as #define on command line. Use this info to improve the "64 bit" detection in extasm.c. (Before it fails with powerpc-ppc64, which has 64-bit int regs but couldn't be detected with #ifdefs.)
| * Issue with packed structs and sizeof, alignof, offsetof in cparser/Xavier Leroy2018-08-173-6/+60
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field): - the reference implementation, in Coq, from cfrontend/Ctypes.v - the implementation used during elaboration, in OCaml, from cparser/Cutil.ml The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used. This causes issues with packed structs. Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs. Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml. For example: ``` struct __packed__(1) s { char c; short s; int i; }; assert (__builtin_offsetof(struct s, i) == 3); assert (sizeof(struct s) = sizeof(char[sizeof(struct s)])); ``` The two assertions fail. In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration. In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs. This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout. Related changes: * cparser/Cutil: add `packing_parameters` function to extract packing info from attributes * cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout * cparser/Elab: check the alignment parameters given in packed attributes. (The check was previously done in cparser/PackedStruct.ml but now it would come too late.) * cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)). * cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab * cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given. Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/. * test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration.
| * Clean .foo.aux files created by coqcXavier Leroy2018-07-101-1/+1
| |
| * Remove the `_Alignas(expr)` construct (#125)Xavier Leroy2018-06-072-36/+32
| | | | | | | | The `_Alignas(expr)` construct is not C11, only `_Alignas(type)` is.
| * Don't depend on ../../clightgenXavier Leroy2018-06-021-3/+3
| | | | | | | | | | It's not really necessary, and under Windows it's really ../../clightgen.exe, which confuses make.
| * Add tests for clightgenXavier Leroy2018-06-015-0/+985
| | | | | | | | Also: add "parallel" entry to test/Makefile for parallel execution of tests.
| * Initialization of anonymous bit-fields in structsXavier Leroy2018-04-251-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For anonymous bit-fields in structs, carrier fields may be introduced which are not initialized since no default initializer are generated earlier. This cause the translation in C2C to throw an error since too few initializers are available. Example: struct s2 { int : 10; int a; int : 10; char b; int : 10; short c; int : 10; } s2 = { 42, 'a', 43 }; To work around this issue we need to generate a default inializer for every new member that does not have a translated member. Based on P#80, with more efficient algorithms. Bug 23362
| * Initialization of union bit fieldsXavier Leroy2018-04-252-0/+33
| | | | | | | | | | | | | | | | | | | | | | Bit fields in unions were initialized like normal fields, causing mismatch on the name of the field. Also: added function Bitfields.carrier_field and refactored. Patch by Bernhard Schommer. Bug 23362
* | Merge branch 'mppa_asmbloc_nobreg' into mppa_k1cCyril SIX2018-11-1484-353/+499
|\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmexpand.ml mppa_k1c/TargetPrinter.ml test/mppa/Makefile test/mppa/builtins/clzll.c test/mppa/generate.sh
| * | Updated Sort Makefile + fixed compilation command bugCyril SIX2018-11-145-62/+123
| | |
| * | Changed mmult to avoid recomputing + fixed potential source of bug in instrCyril SIX2018-11-133-21/+39
| | |
| * | Lancement des tests à partir d'un même scriptCyril SIX2018-11-137-15/+61
| | |
generated by cgit (git 2.34.1) at 2024-07-12 09:15:11 +0000