aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
Commit message (Expand)AuthorAgeFilesLines
* Fixed last instruction not having liveinsCyril SIX2020-07-151-2/+8
* More debug infoCyril SIX2020-07-151-8/+17
* Merge branch 'mppa-RTLpathSE-oracle' of gricad-gitlab.univ-grenoble-alpes.fr:...David Monniaux2020-07-131-3/+13
|\
| * Fix switching basic instruction with IcondCyril SIX2020-07-131-3/+13
* | Merge branch 'mppa-RTLpathSE-oracle' of gricad-gitlab.univ-grenoble-alpes.fr:...David Monniaux2020-07-131-1/+6
|\|
| * 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
|\
| * fix commentSylvain Boulmé2020-06-211-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
* | hsexec_correct proved (under admitted lemmas).Sylvain Boulmé2020-07-031-68/+48
* | Scope issue..Cyril SIX2020-07-031-11/+12
* | Fixing ge, sp, rs, m issueCyril SIX2020-07-031-8/+9
* | fix the proof sketchSylvain Boulmé2020-07-031-30/+22
* | sketch the proof of symbolic execution of one instructionSylvain Boulmé2020-07-032-35/+68
* | slightly simpler codeSylvain Boulmé2020-07-021-64/+88
* | Optimization of Iop symbolic executionSylvain Boulmé2020-07-022-35/+107
* | Fix hypothesis on environment in hsstate_simuSylvain Boulmé2020-07-021-3/+4
* | remove useless (and unprovable) lemmas on completeness of the refinementSylvain Boulmé2020-07-021-47/+66
* | Avancement, mais est-ce prouvable ?Cyril SIX2020-07-011-0/+37
* | hsexec_completeCyril SIX2020-07-011-37/+36
* | AvancementCyril SIX2020-07-012-74/+120
* | hsexec_correctCyril SIX2020-07-012-27/+138
* | Some renamingCyril SIX2020-07-011-38/+49
* | a minor commentSylvain Boulmé2020-06-301-2/+2
* | starting refinement of (abstract) symbolic executionsSylvain Boulmé2020-06-301-0/+160
* | Must generalize silocal_simub with a list of regsCyril SIX2020-06-291-3/+5
* | Only silocal_simub leftCyril SIX2020-06-291-132/+171
generated by cgit (git 2.34.1) at 2024-07-12 03:15:55 +0000