aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
Commit message (Collapse)AuthorAgeFilesLines
...
| | | | * | | | | | | | Fix switching basic instruction with IcondCyril SIX2020-07-131-3/+13
| | | | | | | | | | | |
| | | * | | | | | | | | Merge branch 'mppa-RTLpathSE-oracle' of ↵David Monniaux2020-07-131-1/+6
| | | |\| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-oracle
| | | | * | | | | | | | Fix Icond bugCyril SIX2020-07-131-1/+6
| | | | | | | | | | | |
| | | * | | | | | | | | command line selection of prepass schedulerDavid Monniaux2020-07-114-12/+14
| | | |/ / / / / / / /
| | | * | | | | | | | found another bugDavid Monniaux2020-07-112-2/+3
| | | | | | | | | | |
| | | * | | | | | | | fix the last instruction detection codeDavid Monniaux2020-07-101-2/+5
| | | | | | | | | | |
| | | * | | | | | | | relaxingDavid Monniaux2020-07-101-1/+1
| | | | | | | | | | |
| | | * | | | | | | | relaxing...David Monniaux2020-07-101-2/+2
| | | | | | | | | | |
| | | * | | | | | | | it works but is too constrainedDavid Monniaux2020-07-101-1/+1
| | | | | | | | | | |
| | | * | | | | | | | begin relaxingDavid Monniaux2020-07-101-3/+1
| | | | | | | | | | |
| | | * | | | | | | | oracle super restrictifDavid Monniaux2020-07-101-8/+16
| | | | | | | | | | |
| | | * | | | | | | | proper ordering on calls etc. ?David Monniaux2020-07-101-4/+4
| | | | | | | | | | |
| | | * | | | | | | | trapping opsDavid Monniaux2020-07-101-0/+1
| | | | | | | | | | |
| | | * | | | | | | | trapping loads are irreversibleDavid Monniaux2020-07-102-1/+2
| | | | | | | | | | |
| | | * | | | | | | | Added check on last instructionCyril SIX2020-07-091-1/+19
| | | | | | | | | | |
| | | * | | | | | | | More explicit failwith messages for change_predicted_successorCyril SIX2020-07-081-3/+3
| | | | | | | | | | |
| | | * | | | | | | | Typing informationCyril SIX2020-07-081-4/+8
| | | | | | | | | | |
| | | * | | | | | | | Merge branch 'mppa-RTLpathSE-oracle-outputregs' into mppa-RTLpathSE-oracleCyril SIX2020-07-083-10/+40
| | | |\ \ \ \ \ \ \ \
| | | | * | | | | | | | Output regs in superblocksCyril SIX2020-07-081-4/+9
| | | | | | | | | | | |
| | | | * | | | | | | | print_path_info fixCyril SIX2020-07-081-1/+1
| | | | | | | | | | | |
| | | | * | | | | | | | Output regs in RTLpathCyril SIX2020-07-082-6/+31
| | | | | | | | | | | |
| | | * | | | | | | | | progress on prepass schedulingDavid Monniaux2020-07-081-0/+2
| | | |/ / / / / / / /
| | | * | | | | | | | making progress on prepassDavid Monniaux2020-07-082-8/+26
| | | | | | | | | | |
| | | * | | | | | | | use a command-line optionDavid Monniaux2020-07-081-18/+21
| | | | | | | | | | |
| | | * | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-oracleDavid Monniaux2020-07-081-1/+1
| | | |\ \ \ \ \ \ \ \
| | | * | | | | | | | | prepass reordering activatedDavid Monniaux2020-07-082-12/+36
| | | | | | | | | | | |
| | | * | | | | | | | | begin prepass scheduling oracleDavid Monniaux2020-07-073-14/+426
| | | | | | | | | | | |
| | | * | | | | | | | | begin computing OpWeightsDavid Monniaux2020-07-072-0/+91
| | | | | | | | | | | |
| | * | | | | | | | | | fix phys_eq -> struct_eqSylvain Boulmé2020-07-241-1/+1
| | | | | | | | | | | |
| | * | | | | | | | | | first draft of simu_checkSylvain Boulmé2020-07-241-19/+83
| | | | | | | | | | | |
| | * | | | | | | | | | hsstate_simu_checkSylvain Boulmé2020-07-241-220/+89
| | | | | | | | | | | |
| | * | | | | | | | | | Implem of hsiexit_simu_checkSylvain Boulmé2020-07-241-102/+167
| | | | | | | | | | | |
| | * | | | | | | | | | starting implem of hsilocal_simu_testSylvain Boulmé2020-07-231-119/+75
| | | | | | | | | | | |
| | * | | | | | | | | | Merge branch 'mppa-RTLpathSE-verif' into mppa-RTLpathSE-verif-hash-junkSylvain Boulmé2020-07-232-9/+10
| | |\ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | full symbolic execution with hash-consingSylvain Boulmé2020-07-231-35/+95
| | | | | | | | | | | | |
| | * | | | | | | | | | | symbolic execution of internal nodes with hash-consingSylvain Boulmé2020-07-221-81/+70
| | | | | | | | | | | | |
| | * | | | | | | | | | | Merge branch 'mppa-RTLpathSE-verif' into mppa-RTLpathSE-verif-hash-junkSylvain Boulmé2020-07-221-389/+368
| | |\ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | smart constructors with hash-consingSylvain Boulmé2020-07-221-1/+144
| | | | | | | | | | | | | |
| | * | | | | | | | | | | | Merge branch 'mppa-RTLpathSE-verif' into mppa-RTLpathSE-verif-hash-junkSylvain Boulmé2020-07-222-224/+528
| | |\ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | start a junk implementation of the pre-pass verifierSylvain Boulmé2020-07-222-1/+590
| | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | seval_condition_refines ---> refinement correct only for successful executions ?Cyril SIX2020-07-091-19/+47
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Fixing proofs - back to being able to buildCyril SIX2020-08-181-7/+13
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Propagating changes to hsistate_simu_core_correctCyril SIX2020-08-181-4/+4
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Changing siexit_simu to be able to prove hsiexit_simu_core_correctCyril SIX2020-08-182-12/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Hopefully it's a good change?
| * | | | | | | | | | | | | | One part of hsiexit_simu_core_correctCyril SIX2020-08-181-37/+12
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Proof of hsilocal_simu_core_correctCyril SIX2020-08-181-5/+10
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | None caseCyril SIX2020-08-181-3/+11
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Using PTree.combine to express picking register values from either rs0 or hstCyril SIX2020-08-181-10/+19
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Trying to modify definitions to include list of alive registersCyril SIX2020-08-171-45/+113
| | |_|_|/ / / / / / / / / / | |/| | | | | | | | | | | |
| * | | | | | | | | | | | | generalize builtin_arg_inj into builtin_arg_mapSylvain Boulmé2020-07-232-9/+10
| | |_|/ / / / / / / / / / | |/| | | | | | | | | | |
generated by cgit (git 2.34.1) at 2024-07-12 02:25:16 +0000