aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)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
|\
| * 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
| * Update change log for 3.4, continuedXavier Leroy2018-09-141-2/+5
| * Improved diagnostics: spelling, wording, etc (#138)Michael Schmidt2018-09-145-15/+15
| * Simplified code. Bug 24067Bernhard Schommer2018-09-121-8/+8
| * Tentatively support Coq 8.8.2Xavier Leroy2018-09-121-2/+2
| * 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
| * Fatal error instead of error for bit-fields.Bernhard Schommer2018-09-121-1/+1
| * Attach _Alignas to names and refactor _Alignas checks (#133)Bernhard Schommer2018-09-106-20/+22
| * 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
| * New diagnostic for reduced alignment (#117)Bernhard Schommer2018-08-293-3/+38
| * Bug 24374Bernhard Schommer2018-08-290-0/+0
| * Merge pull request #251 from AbsInt/configure-error-behaviorXavier Leroy2018-08-291-0/+14
| |\
| | * Improve reporting of configuration errorsXavier Leroy2018-08-281-0/+10
| | * Remove leftover Makefile.config before configurationXavier Leroy2018-08-281-0/+4
| * | Bug 24366Bernhard Schommer2018-08-280-0/+0
| * | Import prim token notations before using them, continuedXavier Leroy2018-08-271-0/+1
| * | Import prim token notations before using themJason Gross2018-08-274-1/+4
| * | Bug 24351Bernhard Schommer2018-08-270-0/+0
| |/
| * Make generated file cparser/Parser.v read-onlyXavier Leroy2018-08-271-0/+2
| * Improve execution of regression testsXavier Leroy2018-08-244-16/+45
generated by cgit (git 2.34.1) at 2024-07-06 15:26:00 +0000