aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-2451-320/+693
|\
| * AArch64: normalize function return values of small integer typeXavier Leroy2020-02-211-3/+11
| * Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-215-6/+6
| * Add interoperability test for functions returning small integer typesXavier Leroy2020-02-212-0/+23
| * Support re-normalization of values returned by function callsXavier Leroy2020-02-217-33/+174
| * Refine the type of function results in AST.signatureXavier Leroy2020-02-2143-286/+445
| * More precise determination of small data accesses (#220)Bernhard Schommer2020-02-201-3/+15
| * Support vertical tabs and treat them as whitespace (#218)Bernhard Schommer2020-02-181-1/+1
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-132-2/+3
|\|
| * Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-122-2/+3
* | Added option -ftracelinearize which linearizes based on ifnot branchesCyril SIX2020-02-124-4/+59
* | Moving some arch specific theorems from PSproof to AsmblockpropsCyril SIX2020-02-112-219/+218
* | Moving Asmblockgenproof0 to mppa_k1c/lib/Cyril SIX2020-02-101-0/+0
* | Removing from Asmblockgenproof0 architecture specific definitionsCyril SIX2020-02-109-130/+153
* | Moved some theoremsCyril SIX2020-02-104-113/+101
* | bringing back the ppc64 runtimeDavid Monniaux2020-02-095-0/+440
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2020-02-0817-0/+1430
|\ \
| * | why did we remove the ppc runtime ?!David Monniaux2020-02-0817-0/+1430
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-0812-54/+84
|\ \ \ | |/ / |/| / | |/
| * Added base address if needed.Bernhard Schommer2020-02-063-33/+53
| * Compatibility with OCaml 4.10 (#214)Xavier Leroy2020-02-063-7/+7
| * Revised menhirLib autoconfiguration (#331)Xavier Leroy2020-02-053-5/+9
| * Support Coq 8.11.0 (#212)Xavier Leroy2020-02-054-2/+8
| * Incorrect computation of extra stack size for vararg calls in RISC-V (#213)Bernhard Schommer2020-02-051-2/+2
| * Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
* | stubs to keep compiling on architectures not K1cDavid Monniaux2020-02-075-0/+15
* | Merge branch 'mppa-fixing-bundling' into mppa-workCyril SIX2020-02-064-67/+87
|\ \
| * | Fixing maddw and maddd resource tablesCyril SIX2020-02-061-2/+19
| * | Using Ocaml type instead of string to identify resourcesCyril SIX2020-02-061-35/+36
| * | Fixed reservation tablesCyril SIX2020-02-061-44/+46
| * | Breaking the prologue to satisfy resource constraintsCyril SIX2020-02-061-1/+1
| * | Fixed using ccomp assembly preprocessorCyril SIX2020-02-061-3/+3
| * | Using k1-elf-as instead of k1-cos-gcc for assemblingCyril SIX2020-02-031-2/+2
* | | accessors for records are now not extracted it seemsDavid Monniaux2020-02-061-3/+3
|/ /
* | Added flag to desactivate condition inversionCyril SIX2020-02-033-1/+6
* | Adding threshold to duplicate instructionsCyril SIX2020-01-311-6/+12
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracleCyril SIX2020-01-277-42/+187
|\ \
| * | Updated scripts to run the tests on test/mppaCyril SIX2020-01-275-7/+19
| * | Hardware runs for test/mppa/interopCyril SIX2020-01-271-24/+113
| * | New directive hardtest and hardcheck to run on hardware test/mppa/instrCyril SIX2020-01-271-11/+55
* | | Tail duplication optimization defaulting to offCyril SIX2020-01-272-2/+1
* | | Added a flag to desactivate tail duplicationCyril SIX2020-01-275-6/+17
* | | Added debug message when inverting ifso ifnotCyril SIX2020-01-241-1/+3
* | | Oracle inverting branches when trace does not go in fallthruCyril SIX2020-01-241-2/+21
* | | Revert "Modified the hook for the oracle"Cyril SIX2020-01-233-12/+8
* | | Verificator finished for handling reversed IcondCyril SIX2020-01-232-11/+18
* | | Added clause in match_inst to allow Icond reversalCyril SIX2020-01-231-4/+13
* | | Modified the hook for the oracleCyril SIX2020-01-233-8/+12
* | | Fixing bug caused by get_predecessors returning duplicatesCyril SIX2020-01-231-5/+8
* | | Printing traces right before duplicatingCyril SIX2020-01-231-5/+2
generated by cgit (git 2.34.1) at 2024-07-14 00:58:09 +0000