aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-expect3' into mppa-workDavid Monniaux2020-04-0912-68/+104
|\
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-expect3David Monniaux2020-04-082-156/+151
| |\
| * | __builtin_expect seems to workDavid Monniaux2020-04-078-27/+47
| * | start implementing expect as exprDavid Monniaux2020-04-076-43/+51
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-expectDavid Monniaux2020-04-0675-490/+6684
| |\ \
| * | | __builtin_expect defined as its first argumentDavid Monniaux2019-09-252-1/+9
* | | | Merge remote-tracking branch 'origin/mppa-thread' into mppa-workDavid Monniaux2020-04-093-2/+3
|\ \ \ \
| * \ \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-0837-501/+1069
| |\ \ \ \ | | | |_|/ | | |/| |
| * | | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-2514-95/+106
| |\ \ \ \
| | * | | | rm commented out blockDavid Monniaux2020-02-241-32/+0
| | * | | | during merge; still some typing issuesDavid Monniaux2020-02-242-10/+12
| | * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2020-02-242-0/+2166
| | |\ \ \ \
| | * \ \ \ \ Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-2414-85/+126
| | |\ \ \ \ \
| * | | | | | | fixes for aarch64 arm ppc ppc64David Monniaux2020-02-241-1/+1
| * | | | | | | thread local declarations now workDavid Monniaux2020-02-242-1/+2
| | |_|/ / / / | |/| | | | |
* | | | | | | Merge remote-tracking branch 'origin/mppa-cse2' into mppa-workDavid Monniaux2020-04-098-114/+2687
|\ \ \ \ \ \ \
| * | | | | | | fix Icond now has a extra argumentDavid Monniaux2020-04-082-3/+3
| * | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-04-0832-333/+532
| |\ \ \ \ \ \ \ | | | |_|_|/ / / | | |/| | | | |
| * | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-311-25/+25
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ 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
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David 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
generated by cgit (git 2.34.1) at 2024-06-02 22:41:42 +0000