aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* Adding copyrightsCyril SIX2020-05-0456-457/+755
* Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-217-147/+386
|\
| * Merge branch 'mppa-notrap-semantics' of ../mppa-notrap-semantics into mppa-licmDavid Monniaux2020-04-207-147/+386
| |\
| | * new semantics for some trapping operationsDavid Monniaux2020-04-205-79/+26
| | * detail with shrxlDavid Monniaux2020-04-201-2/+4
| | * adapt VADavid Monniaux2020-04-201-8/+306
| | * change semantics for trapping opsDavid Monniaux2020-04-201-58/+50
* | | Merge remote-tracking branch 'origin/mppa-fast-div' into mppa-featuresDavid Monniaux2020-04-203-16/+68
|\ \ \
| * \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2020-04-2056-6790/+8851
| |\ \ \ | | | |/ | | |/|
| * | | added -fdiv-i32 and -fdiv-i64 optionsDavid Monniaux2019-05-291-2/+8
| * | | arranging for selection of divisor as optionDavid Monniaux2019-05-291-4/+44
| * | | Merge remote-tracking branch 'origin/mppa-cos' into mppa-fast-divDavid Monniaux2019-05-291-5/+5
| |\ \ \
| * \ \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-295-2/+2
| |\ \ \ \
| * \ \ \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-215-934/+695
| |\ \ \ \ \
| * \ \ \ \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-201-0/+3
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-177-298/+593
| |\ \ \ \ \ \ \
| * | | | | | | | sdiv seems to work, udiv/umod/smod BOGUSDavid Monniaux2019-05-162-12/+18
* | | | | | | | | 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
generated by cgit (git 2.34.1) at 2024-06-02 21:11:06 +0000