aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Added printf to the unitary tests for instructionsCyril SIX2018-12-072-27/+29
|
* Fixed that fnegd and negd had been invertedCyril SIX2018-12-071-1/+1
|
* Fixed bundles (back to 1 instruction per bundle)Cyril SIX2018-12-071-65/+65
|
* Added a printf wrapper in test/mppa/libCyril SIX2018-12-074-0/+160
|
* Introducing ;; as Pcomma in Asm.vCyril SIX2018-12-032-65/+67
|
* Finished implementation of va_arg + testing doneCyril SIX2018-11-305-9/+85
|
* Wrote some tests on va_arg, need to implement __compcert_va_int32 & cieCyril SIX2018-11-283-12/+471
|
* Added a jobs parameter to the test scriptsCyril SIX2018-11-284-7/+13
|
* mppa_k1c compilesCyril SIX2018-11-282-9/+3
|
* Merge branch 'mppa_k1c' into works_for_x86_not_for_k1Cyril SIX2018-11-289-18/+238
|\
| * 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
| |
* | compilation Asmexpandaux both for x86/ and mppa_k1c/Sylvain Boulmé2018-11-286-5/+17
| |
* | Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-274-10/+19
| |
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-268-22/+16
|/
* Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-265-1588/+9
|
* 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
|
* Changed ABI to match GCC - interoperability not tested yetCyril SIX2018-11-237-167/+170
|
* Mise à jour vis à vis de CompCert 3.4Cyril SIX2018-11-217-10/+51
|
* Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-21126-2299/+4255
|\ | | | | | | | | Conflicts: .gitignore
| * Updates for release 3.4v3.4Xavier Leroy2018-09-172-2/+2
| |
| * Bug 24510Bernhard Schommer2018-09-140-0/+0
| |
| * flocq: minor cleaning (#257)Vincent Laporte2018-09-141-3/+2
| | | | | | | | | | | | This change avoids relying on generated names, making the proof script compatible with ongoing evolutions of the `zify` tactic. A similar cleanup was already performed in Flocq's master sources.
| * Update change log for 3.4, continuedXavier Leroy2018-09-141-2/+5
| |
| * Improved diagnostics: spelling, wording, etc (#138)Michael Schmidt2018-09-145-15/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * bug 24268: avoid assertion after reporting error for invalid call to builtin_debug * bug 24268, remove duplicated warning tag in lexer messages * bug 24268, fix spelling in array element designator message * bug 24268, unify 'consider adding option ...' messages * bug 24268, add spacing for icbi operands * bug 24268, uniform use of Ignored_attributes class for identical warnings * bug 24268, unify message for 'assignment to const type' to error from error/fatal error * bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized"
| * Simplified code. Bug 24067Bernhard Schommer2018-09-121-8/+8
| |
| * Tentatively support Coq 8.8.2Xavier Leroy2018-09-121-2/+2
| | | | | | | | | | It's not out yet, but based on the state of the v8.8 branch of Coq, it is very likely to be compatible with CompCert.
| * Typo in OCaml version numberXavier Leroy2018-09-121-1/+1
| |
| * Update version and change log in preparation for public release 3.4Xavier Leroy2018-09-122-1/+63
| |
| * Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-1214-28/+64
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Generate a nop instruction after ais annotations. In order to prevent the merging of ais annotations with following Labels a nop instruction is inserted, but only if the annotation is followed immediately by a label. The insertion of nop instructions is performed during the expansion of builtin and pseudo assembler instructions and is processor independent, by inserting a __builtin_nop built-in. * Add Pnop instruction to ARM, RISC-V, and x86 ARM as well as RISC-V don't have nop instructions that can be easily encoded by for example add with zero instructions. For x86 we used to use `mov X0, X0` for nop but this may not be as efficient as the true nop instruction. * Implement __builtin_nop on all supported target architectures. This builtin is not yet made available on the C side for all architectures. Bug 24067
| * Fatal error instead of error for bit-fields.Bernhard Schommer2018-09-121-1/+1
| | | | | | | | | | | | Since the following offsetof cannot handle bit-fields we should stop earlier. Bug 24480
| * Attach _Alignas to names and refactor _Alignas checks (#133)Bernhard Schommer2018-09-106-20/+22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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.
| * Ignore generated conflict file. Bug 24455Bernhard Schommer2018-09-101-0/+1
| |
| * Bug 23389Bernhard Schommer2018-09-040-0/+0
| |
| * Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2018-09-041-1/+1
| |\
| | * Typo in commentXavier Leroy2018-09-031-1/+1
| | |
| * | document new named warning class 'reduced-alignment', bug 23389Michael Schmidt2018-09-041-0/+4
| |/
| * Move parameter check.Bernhard Schommer2018-09-031-2/+6
| | | | | | | | | | | | Instead of performing the check only for parameters of function definitions also perform it for function declarations. Bug 23393
| * New diagnostic for reduced alignment (#117)Bernhard Schommer2018-08-293-3/+38
| | | | | | | | | | | | | | The new diagnostic triggers if an `_Alignas` or an `aligned` attribute or a `packed` attribute requests an alignment smaller than the natural alignment. Bug 23389
| * Bug 24374Bernhard Schommer2018-08-290-0/+0
| |
| * Merge pull request #251 from AbsInt/configure-error-behaviorXavier Leroy2018-08-291-0/+14
| |\ | | | | | | Improve behavior of configure script in case of configuration errors
| | * Improve reporting of configuration errorsXavier Leroy2018-08-281-0/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The full "usage" text is so long that the actual error message scrolls off the screen. With this commit, instead, a short (3-line) error message is printed, with a suggestion to do `./configure -help`. The whole "usage" text is printed by `./configure -help`. Also: better error message for unknown options (arguments starting with `-`).
| | * Remove leftover Makefile.config before configurationXavier Leroy2018-08-281-0/+4
| | | | | | | | | | | | | | | | | | | | | So that if an error occurs during configuration, there is no Makefile.config file and "make" will fail. Closes: #244
| * | Bug 24366Bernhard Schommer2018-08-280-0/+0
| | |
| * | Import prim token notations before using them, continuedXavier Leroy2018-08-271-0/+1
| | | | | | | | | | | | | | | Follow-up to f6f537d. "list" scope must be opened to counterbalance opening of "string" scope.
| * | Import prim token notations before using themJason Gross2018-08-274-1/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. Closes #246 Closes #250
| * | Bug 24351Bernhard Schommer2018-08-270-0/+0
| |/
| * Make generated file cparser/Parser.v read-onlyXavier Leroy2018-08-271-0/+2
| | | | | | | | | | | | | | For consistency with other generated .v files, and because it protects against editing the generated file, see Github issue #248. Closes: #248
| * 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
generated by cgit (git 2.34.1) at 2024-07-11 23:16:19 +0000