aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workv3.6_mppa_2019-09-20David Monniaux2019-09-2086-300/+16263
|\
| * fix compiling for aarch64David Monniaux2019-09-204-4/+42
| * fix compilingDavid Monniaux2019-09-204-3/+8
| * extraction problemsDavid Monniaux2019-09-202-2/+2
| * Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-2082-298/+16217
| |\
| | * Update for release 3.6v3.6Xavier Leroy2019-09-171-2/+3
| | * Revise the "bench" entries of the test suiteXavier Leroy2019-09-175-12/+110
| | * Updates in preparation for release 3.6Xavier Leroy2019-09-162-1/+63
| | * -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
| | * clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-163-16/+35
| | * Reworked json export.Bernhard Schommer2019-09-125-78/+91
| | * Asmgenproof1: useless unfolding in proof scripts causing "omega" to failXavier Leroy2019-09-111-3/+3
| | * Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-1163-167/+15898
| | |\
| | | * AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}xavier.leroy2019-08-312-4/+4
| | | * Offset out of range for ldp/stp instructionsxavier.leroy2019-08-231-1/+3
| | | * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-176-16/+16
| | | * Test for the compilation of floating-point literalsXavier Leroy2019-08-083-1/+562
| | | * AArch64 portXavier Leroy2019-08-0848-87/+14874
| | | * Relax lemma Val.zero_ext_and and add Val.zero_ext_andlXavier Leroy2019-08-071-2/+10
| | | * Factor out endianness determination between testsXavier Leroy2019-08-074-30/+14
| | | * ndfun: add support for guards on patternsXavier Leroy2019-08-071-5/+16
| | | * More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
| | | * Errors: fixed a loop in tactic MonadInvXavier Leroy2019-08-071-1/+1
| | | * Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
| | | * Values: add functions for zero- and sign-extension of 64-bit integersXavier Leroy2019-08-071-0/+12
| | | * Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
| | | * Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
| | | * Define integer sign extension for zero bitsXavier Leroy2019-08-072-42/+57
| | | * Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
| | | * x86: wrong expansion of __builtin_fmadd et alXavier Leroy2019-08-071-13/+19
| | | * Add support for Coq 8.10Xavier Leroy2019-08-071-2/+2
| | | * Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-071-0/+1
| | | * Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-071-1/+1
| | | * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-078-23/+22
| | | * Simplify invocation of Emacs + Proof GeneralXavier Leroy2019-08-071-17/+3
* | | | More work on test, regression/packedstruct1.c and regression/varargs2.c don't...Cyril SIX2019-09-204-24/+33
* | | | Adding SIMU=k1-cluster -- in configureCyril SIX2019-09-201-0/+1
|/ / /
* | | __builtin_bswap16, 32 and 64Cyril SIX2019-09-204-39/+38
* | | Fixing machine description (error in wchar signedness + trying different valu...Cyril SIX2019-09-191-5/+32
* | | Desactivating CompCert tests taking too longCyril SIX2019-09-191-1/+3
* | | Adding some function calls in interop testsCyril SIX2019-09-192-7/+15
* | | Detailing oracle/vérificateur in the timingsCyril SIX2019-09-182-2/+3
* | | Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-184-7/+10
* | | Compatibility fix for Coq 8.7.1Cyril SIX2019-09-131-3/+3
* | | Adding back "exit 2" to the test target of test/c/MakefileCyril SIX2019-09-131-2/+2
* | | Scaling down compression testsCyril SIX2019-09-131-5/+11
* | | Reducing further the input size of the testsCyril SIX2019-09-1330-71/+68
* | | Scaling down most of c/ CompCert testsCyril SIX2019-09-1318-37/+56
* | | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-09-1025-107/+559
|\ \ \
| * | | Starting to modify official CompCert tests to be passable with the simuCyril SIX2019-09-1018-89/+81
generated by cgit (git 2.34.1) at 2024-05-20 11:32:43 +0000