Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-21 | 7 | -147/+386 |
|\ | |||||
| * | Merge branch 'mppa-notrap-semantics' of ../mppa-notrap-semantics into mppa-licm | David Monniaux | 2020-04-20 | 7 | -147/+386 |
| |\ | |||||
| | * | new semantics for some trapping operations | David Monniaux | 2020-04-20 | 5 | -79/+26 |
| | * | detail with shrxl | David Monniaux | 2020-04-20 | 1 | -2/+4 |
| | * | adapt VA | David Monniaux | 2020-04-20 | 1 | -8/+306 |
| | * | change semantics for trapping ops | David Monniaux | 2020-04-20 | 1 | -58/+50 |
* | | | Merge remote-tracking branch 'origin/mppa-fast-div' into mppa-features | David Monniaux | 2020-04-20 | 3 | -16/+68 |
|\ \ \ | |||||
| * \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div | David Monniaux | 2020-04-20 | 56 | -6790/+8851 |
| |\ \ \ | | | |/ | | |/| | |||||
| * | | | added -fdiv-i32 and -fdiv-i64 options | David Monniaux | 2019-05-29 | 1 | -2/+8 |
| * | | | arranging for selection of divisor as option | David Monniaux | 2019-05-29 | 1 | -4/+44 |
| * | | | Merge remote-tracking branch 'origin/mppa-cos' into mppa-fast-div | David Monniaux | 2019-05-29 | 1 | -5/+5 |
| |\ \ \ | |||||
| * \ \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div | David Monniaux | 2019-05-29 | 5 | -2/+2 |
| |\ \ \ \ | |||||
| * \ \ \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div | David Monniaux | 2019-05-21 | 5 | -934/+695 |
| |\ \ \ \ \ | |||||
| * \ \ \ \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div | David Monniaux | 2019-05-20 | 1 | -0/+3 |
| |\ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div | David Monniaux | 2019-05-17 | 7 | -298/+593 |
| |\ \ \ \ \ \ \ | |||||
| * | | | | | | | | sdiv seems to work, udiv/umod/smod BOGUS | David Monniaux | 2019-05-16 | 2 | -12/+18 |
* | | | | | | | | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-20 | 4 | -20/+46 |
|\ \ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|/ | |/| | | | | | | | |||||
| * | | | | | | | | add options for controlling madd and notrap selection | David Monniaux | 2020-04-19 | 2 | -15/+34 |
| * | | | | | | | | test whether the instructions are allowed | David Monniaux | 2020-04-19 | 1 | -2/+4 |
| * | | | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-licm | David Monniaux | 2020-04-01 | 1 | -3/+4 |
| |\ \ \ \ \ \ \ \ | | | |_|_|_|_|_|/ | | |/| | | | | | | |||||
| * | | | | | | | | lemma on stepping through non trapping instructions | David Monniaux | 2020-03-30 | 1 | -3/+8 |
* | | | | | | | | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features | David Monniaux | 2020-04-12 | 3 | -2/+30 |
|\ \ \ \ \ \ \ \ \ | |||||
| * | | | | | | | | | fix for k1c | David Monniaux | 2020-04-11 | 1 | -1/+1 |
| * | | | | | | | | | fix writing profiling info for Aarch64 | David Monniaux | 2020-04-10 | 1 | -1/+1 |
| * | | | | | | | | | various fixes for aarch64 profiling | David Monniaux | 2020-04-10 | 1 | -1/+1 |
| * | | | | | | | | | moved to common place | David Monniaux | 2020-04-10 | 1 | -52/+0 |
| * | | | | | | | | | begin factorizing profiler | David Monniaux | 2020-04-10 | 1 | -10/+18 |
| * | | | | | | | | | fixed a bug in support libraries; reload profiling info | David Monniaux | 2020-04-08 | 1 | -1/+1 |
| * | | | | | | | | | library support for writing profiling information to files | David Monniaux | 2020-04-08 | 1 | -4/+17 |
| * | | | | | | | | | print profiling ids | David Monniaux | 2020-04-08 | 1 | -3/+23 |
| * | | | | | | | | | looks like it works? | David Monniaux | 2020-04-08 | 2 | -4/+39 |
| * | | | | | | | | | print hashes | David Monniaux | 2020-04-08 | 1 | -2/+2 |
| * | | | | | | | | | so that it gets printed | David Monniaux | 2020-04-08 | 1 | -0/+3 |
| * | | | | | | | | | added EF_profiling | David Monniaux | 2020-04-08 | 1 | -0/+1 |
| | |/ / / / / / / | |/| | | | | | | | |||||
* | | | | | | | | | update it's now @tlsle not @tprel | David Monniaux | 2020-04-09 | 1 | -2/+4 |
* | | | | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-thread | David Monniaux | 2020-04-08 | 17 | -119/+270 |
|\| | | | | | | | | |||||
| * | | | | | | | | Fix cutrewrite deprecated | Cyril SIX | 2020-04-01 | 1 | -3/+4 |
| |/ / / / / / / | |||||
| * | | | | | | | proof clarification | David Monniaux | 2020-03-20 | 1 | -3/+5 |
| * | | | | | | | more understandabe proofs | David Monniaux | 2020-03-20 | 1 | -38/+38 |
| * | | | | | | | progress in RA invariants | David Monniaux | 2020-03-20 | 1 | -23/+24 |
| * | | | | | | | Duplicate: getting rid of the annoying exception-based code | Cyril SIX | 2020-03-09 | 1 | -7/+2 |
| * | | | | | | | removing more coq8.10 warnings | Sylvain Boulmé | 2020-03-09 | 4 | -2/+10 |
| * | | | | | | | removing some coqc 8.10 warnings | Sylvain Boulmé | 2020-03-09 | 1 | -4/+4 |
| * | | | | | | | removing warnings on hints in core | Sylvain Boulmé | 2020-03-07 | 11 | -42/+39 |
| * | | | | | | | forgot k1C | David Monniaux | 2020-03-03 | 2 | -0/+147 |
| * | | | | | | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2020-03-03 | 2 | -17/+26 |
* | | | | | | | | Merge branch 'mppa-work' into mppa-thread | Cyril SIX | 2020-02-25 | 2 | -17/+26 |
|\ \ \ \ \ \ \ \ | |||||
| * | | | | | | | | fixed typing issues | David Monniaux | 2020-02-24 | 1 | -1/+1 |
| * | | | | | | | | during merge; still some typing issues | David Monniaux | 2020-02-24 | 2 | -6/+9 |
| * | | | | | | | | fix | David Monniaux | 2020-02-24 | 1 | -4/+5 |