aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-204-20/+46
|\
| * add options for controlling madd and notrap selectionDavid Monniaux2020-04-192-15/+34
| * test whether the instructions are allowedDavid Monniaux2020-04-191-2/+4
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-licmDavid Monniaux2020-04-011-3/+4
| |\
| * | lemma on stepping through non trapping instructionsDavid Monniaux2020-03-301-3/+8
* | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-123-2/+30
|\ \ \
| * | | fix for k1cDavid Monniaux2020-04-111-1/+1
| * | | fix writing profiling info for Aarch64David Monniaux2020-04-101-1/+1
| * | | various fixes for aarch64 profilingDavid Monniaux2020-04-101-1/+1
| * | | moved to common placeDavid Monniaux2020-04-101-52/+0
| * | | begin factorizing profilerDavid Monniaux2020-04-101-10/+18
| * | | fixed a bug in support libraries; reload profiling infoDavid Monniaux2020-04-081-1/+1
| * | | library support for writing profiling information to filesDavid Monniaux2020-04-081-4/+17
| * | | print profiling idsDavid Monniaux2020-04-081-3/+23
| * | | looks like it works?David Monniaux2020-04-082-4/+39
| * | | print hashesDavid Monniaux2020-04-081-2/+2
| * | | so that it gets printedDavid Monniaux2020-04-081-0/+3
| * | | added EF_profilingDavid Monniaux2020-04-081-0/+1
| | |/ | |/|
* | | update it's now @tlsle not @tprelDavid Monniaux2020-04-091-2/+4
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-0817-119/+270
|\| |
| * | Fix cutrewrite deprecatedCyril SIX2020-04-011-3/+4
| |/
| * proof clarificationDavid Monniaux2020-03-201-3/+5
| * more understandabe proofsDavid Monniaux2020-03-201-38/+38
| * progress in RA invariantsDavid Monniaux2020-03-201-23/+24
| * Duplicate: getting rid of the annoying exception-based codeCyril SIX2020-03-091-7/+2
| * removing more coq8.10 warningsSylvain Boulmé2020-03-094-2/+10
| * removing some coqc 8.10 warningsSylvain Boulmé2020-03-091-4/+4
| * removing warnings on hints in coreSylvain Boulmé2020-03-0711-42/+39
| * forgot k1CDavid Monniaux2020-03-032-0/+147
| * Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-032-17/+26
* | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-252-17/+26
|\ \
| * | fixed typing issuesDavid Monniaux2020-02-241-1/+1
| * | during merge; still some typing issuesDavid Monniaux2020-02-242-6/+9
| * | fixDavid Monniaux2020-02-241-4/+5
| * | fixDavid Monniaux2020-02-241-7/+12
| |/
* | thread local declarations now workDavid Monniaux2020-02-241-2/+6
* | it now works, no more ugly hack to access thread local dataDavid Monniaux2020-02-241-4/+8
|/
* 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-108-129/+152
* Moved some theoremsCyril SIX2020-02-104-113/+101
* 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
* Merge branch 'mppa-work' into mppa-duplicate-oracleCyril SIX2020-01-221-0/+132
|\
| * Fixing issue with "destruct ... in ..." tactics with Coq 8.8Cyril SIX2020-01-091-5/+5
| * swap load and store at disjoint offsetsDavid Monniaux2019-12-161-1/+53
| * swap stores at disjoint offsetsDavid Monniaux2019-12-161-16/+30
| * comment out theorem that cannot be provedDavid Monniaux2019-12-141-29/+33
generated by cgit (git 2.34.1) at 2024-06-03 03:23:22 +0000