Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| | * | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash... | David Monniaux | 2020-07-30 | 7 | -165/+140 | |
| | |\ \ \ \ \ \ \ \ | | | |/ / / / / / / | | |/| | | | | | | | ||||||
| | * | | | | | | | | trace quand le simulateur est appele | Sylvain Boulmé | 2020-07-24 | 1 | -2/+3 | |
| | * | | | | | | | | Merge branch 'mppa-RTLpathSE-oracle' into mppa-RTLpathSE-verif-hash-junk | Cyril SIX | 2020-07-24 | 9 | -47/+768 | |
| | |\ \ \ \ \ \ \ \ | ||||||
| | | * | | | | | | | | More robust code for changing order of instructions | Cyril SIX | 2020-07-20 | 1 | -43/+118 | |
| | | * | | | | | | | | Fixed last instruction not having liveins | Cyril SIX | 2020-07-15 | 1 | -2/+8 | |
| | | * | | | | | | | | More debug info | Cyril SIX | 2020-07-15 | 1 | -8/+17 | |
| | | * | | | | | | | | Merge branch 'mppa-RTLpathSE-oracle' of gricad-gitlab.univ-grenoble-alpes.fr:... | David Monniaux | 2020-07-13 | 1 | -3/+13 | |
| | | |\ \ \ \ \ \ \ \ | ||||||
| | | | * | | | | | | | | Fix switching basic instruction with Icond | Cyril SIX | 2020-07-13 | 1 | -3/+13 | |
| | | * | | | | | | | | | Merge branch 'mppa-RTLpathSE-oracle' of gricad-gitlab.univ-grenoble-alpes.fr:... | David Monniaux | 2020-07-13 | 1 | -1/+6 | |
| | | |\| | | | | | | | | ||||||
| | | | * | | | | | | | | Fix Icond bug | Cyril SIX | 2020-07-13 | 1 | -1/+6 | |
| | | * | | | | | | | | | command line selection of prepass scheduler | David Monniaux | 2020-07-11 | 4 | -12/+14 | |
| | | |/ / / / / / / / | ||||||
| | | * | | | | | | | | found another bug | David Monniaux | 2020-07-11 | 2 | -2/+3 | |
| | | * | | | | | | | | fix the last instruction detection code | David Monniaux | 2020-07-10 | 1 | -2/+5 | |
| | | * | | | | | | | | relaxing | David Monniaux | 2020-07-10 | 1 | -1/+1 | |
| | | * | | | | | | | | relaxing... | David Monniaux | 2020-07-10 | 1 | -2/+2 | |
| | | * | | | | | | | | it works but is too constrained | David Monniaux | 2020-07-10 | 1 | -1/+1 | |
| | | * | | | | | | | | begin relaxing | David Monniaux | 2020-07-10 | 1 | -3/+1 | |
| | | * | | | | | | | | oracle super restrictif | David Monniaux | 2020-07-10 | 1 | -8/+16 | |
| | | * | | | | | | | | proper ordering on calls etc. ? | David Monniaux | 2020-07-10 | 1 | -4/+4 | |
| | | * | | | | | | | | trapping ops | David Monniaux | 2020-07-10 | 1 | -0/+1 | |
| | | * | | | | | | | | trapping loads are irreversible | David Monniaux | 2020-07-10 | 2 | -1/+2 | |
| | | * | | | | | | | | Added check on last instruction | Cyril SIX | 2020-07-09 | 1 | -1/+19 | |
| | | * | | | | | | | | More explicit failwith messages for change_predicted_successor | Cyril SIX | 2020-07-08 | 1 | -3/+3 | |
| | | * | | | | | | | | Typing information | Cyril SIX | 2020-07-08 | 1 | -4/+8 | |
| | | * | | | | | | | | Merge branch 'mppa-RTLpathSE-oracle-outputregs' into mppa-RTLpathSE-oracle | Cyril SIX | 2020-07-08 | 3 | -10/+40 | |
| | | |\ \ \ \ \ \ \ \ | ||||||
| | | | * | | | | | | | | Output regs in superblocks | Cyril SIX | 2020-07-08 | 1 | -4/+9 | |
| | | | * | | | | | | | | print_path_info fix | Cyril SIX | 2020-07-08 | 1 | -1/+1 | |
| | | | * | | | | | | | | Output regs in RTLpath | Cyril SIX | 2020-07-08 | 2 | -6/+31 | |
| | | * | | | | | | | | | progress on prepass scheduling | David Monniaux | 2020-07-08 | 1 | -0/+2 | |
| | | |/ / / / / / / / | ||||||
| | | * | | | | | | | | making progress on prepass | David Monniaux | 2020-07-08 | 2 | -8/+26 | |
| | | * | | | | | | | | use a command-line option | David Monniaux | 2020-07-08 | 1 | -18/+21 | |
| | | * | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-oracle | David Monniaux | 2020-07-08 | 1 | -1/+1 | |
| | | |\ \ \ \ \ \ \ \ | ||||||
| | | * | | | | | | | | | prepass reordering activated | David Monniaux | 2020-07-08 | 2 | -12/+36 | |
| | | * | | | | | | | | | begin prepass scheduling oracle | David Monniaux | 2020-07-07 | 3 | -14/+426 | |
| | | * | | | | | | | | | begin computing OpWeights | David Monniaux | 2020-07-07 | 2 | -0/+91 | |
| | * | | | | | | | | | | fix phys_eq -> struct_eq | Sylvain Boulmé | 2020-07-24 | 1 | -1/+1 | |
| | * | | | | | | | | | | first draft of simu_check | Sylvain Boulmé | 2020-07-24 | 1 | -19/+83 | |
| | * | | | | | | | | | | hsstate_simu_check | Sylvain Boulmé | 2020-07-24 | 1 | -220/+89 | |
| | * | | | | | | | | | | Implem of hsiexit_simu_check | Sylvain Boulmé | 2020-07-24 | 1 | -102/+167 | |
| | * | | | | | | | | | | starting implem of hsilocal_simu_test | Sylvain Boulmé | 2020-07-23 | 1 | -119/+75 | |
| | * | | | | | | | | | | Merge branch 'mppa-RTLpathSE-verif' into mppa-RTLpathSE-verif-hash-junk | Sylvain Boulmé | 2020-07-23 | 2 | -9/+10 | |
| | |\ \ \ \ \ \ \ \ \ \ | ||||||
| | * | | | | | | | | | | | full symbolic execution with hash-consing | Sylvain Boulmé | 2020-07-23 | 1 | -35/+95 | |
| | * | | | | | | | | | | | symbolic execution of internal nodes with hash-consing | Sylvain Boulmé | 2020-07-22 | 1 | -81/+70 | |
| | * | | | | | | | | | | | Merge branch 'mppa-RTLpathSE-verif' into mppa-RTLpathSE-verif-hash-junk | Sylvain Boulmé | 2020-07-22 | 1 | -389/+368 | |
| | |\ \ \ \ \ \ \ \ \ \ \ | ||||||
| | * | | | | | | | | | | | | smart constructors with hash-consing | Sylvain Boulmé | 2020-07-22 | 1 | -1/+144 | |
| | * | | | | | | | | | | | | Merge branch 'mppa-RTLpathSE-verif' into mppa-RTLpathSE-verif-hash-junk | Sylvain Boulmé | 2020-07-22 | 2 | -224/+528 | |
| | |\ \ \ \ \ \ \ \ \ \ \ \ | ||||||
| | * | | | | | | | | | | | | | start a junk implementation of the pre-pass verifier | Sylvain Boulmé | 2020-07-22 | 2 | -1/+590 | |
| | * | | | | | | | | | | | | | seval_condition_refines ---> refinement correct only for successful executions ? | Cyril SIX | 2020-07-09 | 1 | -19/+47 | |
| * | | | | | | | | | | | | | | Fixing proofs - back to being able to build | Cyril SIX | 2020-08-18 | 1 | -7/+13 | |
| * | | | | | | | | | | | | | | Propagating changes to hsistate_simu_core_correct | Cyril SIX | 2020-08-18 | 1 | -4/+4 |