aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-311-25/+25
|\
| * forgot an 'Admitted'David Monniaux2020-03-311-1/+1
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-03-312-10/+17
| |\
| * \ Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-03-115-128/+366
| |\ \
| * | | same version as in dm-cse2David Monniaux2020-03-031-24/+24
* | | | Merge branch 'mppa-cse3' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-312-0/+292
|\ \ \ \
| * | | | pass to insert a "nop" at head of each functionDavid Monniaux2020-03-282-1/+275
| * | | | pass to insert a nop at start position in functionsDavid Monniaux2020-03-271-0/+18
* | | | | no more admittedDavid Monniaux2020-03-311-1/+4
|/ / / /
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-171-7/+11
|\ \ \ \ | | |_|/ | |/| |
| * | | Desactivating branch predictions by defaultCyril SIX2020-03-171-7/+11
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-151-3/+6
|\| | |
| * | | more inliningDavid Monniaux2020-03-151-3/+6
| | |/ | |/|
* | | CSE3 alias analysisDavid Monniaux2020-03-143-4/+62
* | | is_trivial_op in CSE3David Monniaux2020-03-141-4/+16
* | | no more 'admit' in CSE3David Monniaux2020-03-141-2/+4
* | | Iload notrapDavid Monniaux2020-03-141-2/+101
* | | IreturnDavid Monniaux2020-03-141-2/+1
* | | IreturnDavid Monniaux2020-03-141-7/+7
* | | IjumptableDavid Monniaux2020-03-141-3/+4
* | | IcondDavid Monniaux2020-03-141-3/+4
* | | ItailcallDavid Monniaux2020-03-141-3/+19
* | | IcallDavid Monniaux2020-03-141-1/+13
* | | moving forward in loadsDavid Monniaux2020-03-131-2/+52
* | | moving forward but could be simplifiedDavid Monniaux2020-03-131-26/+64
* | | CSE3 proofs: REL is inductiveDavid Monniaux2020-03-131-1/+13
* | | moving forward in proofsDavid Monniaux2020-03-131-1/+20
* | | progress in proofsDavid Monniaux2020-03-131-17/+8
* | | moving forward in proofsDavid Monniaux2020-03-132-3/+115
* | | progress on inductiveness proofDavid Monniaux2020-03-131-2/+18
* | | some automationDavid Monniaux2020-03-132-29/+64
* | | some progress (but broken proof)David Monniaux2020-03-131-36/+87
* | | begin adding invariants and inductivenessDavid Monniaux2020-03-131-9/+17
* | | fmap_semDavid Monniaux2020-03-132-4/+68
* | | inductiveDavid Monniaux2020-03-131-0/+13
* | | proof sketch for CSE3 stepsDavid Monniaux2020-03-122-10/+244
* | | begin writing match states predicatesDavid Monniaux2020-03-122-27/+59
* | | CSE3 analysisDavid Monniaux2020-03-123-6/+81
* | | inductiveness test in CSE3David Monniaux2020-03-123-4/+31
* | | removed second analysis phaseDavid Monniaux2020-03-124-30/+24
* | | typing and store stuffDavid Monniaux2020-03-124-61/+91
* | | store soundDavid Monniaux2020-03-122-1/+24
* | | more lemmasDavid Monniaux2020-03-122-8/+45
* | | lemmas on storevDavid Monniaux2020-03-122-0/+61
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-115-128/+366
|\| |
| * | Fixed stupid typo bug preventing the prediction update for the RANDOM predictorCyril SIX2020-03-111-1/+1
| * | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-112-125/+360
| |\ \
| | * | Linearizeaux: dumb selector when cycling dependencies are foundCyril SIX2020-03-101-4/+6
| | * | Linearizeaux, forgot to visit the rest of the nodes in dfs_visitCyril SIX2020-03-101-22/+26
| | * | Some dependencies were not taken into account in tracelinearizeCyril SIX2020-03-101-15/+12
generated by cgit (git 2.34.1) at 2024-06-12 05:44:50 +0000