index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
scheduling
Commit message (
Expand
)
Author
Age
Files
Lines
*
some advance in main liveness lemmas
Léo Gourdin
2021-06-02
1
-28
/
+68
*
Some others main lemmas
Léo Gourdin
2021-06-01
1
-7
/
+33
*
preparing liveness proof main theorem
Léo Gourdin
2021-06-01
1
-2
/
+43
*
Lemma liveness_checker_correct
Léo Gourdin
2021-06-01
1
-0
/
+12
*
Lemma list_iblock_checker_correct
Léo Gourdin
2021-06-01
1
-0
/
+20
*
Dupmap bugfix and some advance in Livegen
Léo Gourdin
2021-05-31
4
-29
/
+89
*
prove fsem2cfgsem_ibistep_simu
Sylvain Boulmé
2021-05-31
1
-19
/
+13
*
BTL Scheduler oracle and some drafts
Léo Gourdin
2021-05-31
5
-12
/
+91
*
BTLroadmap: jumptable
Sylvain Boulmé
2021-05-29
1
-1
/
+1
*
maj roadmap
Sylvain Boulmé
2021-05-28
1
-36
/
+32
*
declare a checker for the symbolic simulation
Sylvain Boulmé
2021-05-28
1
-2
/
+13
*
remove dupmap from BTL_Scheduler !
Sylvain Boulmé
2021-05-28
3
-36
/
+22
*
archi pour la verif du scheduler
Sylvain Boulmé
2021-05-28
3
-11
/
+82
*
starting to extend RTLtoBTL with Liveness checking (on BTL side)
Sylvain Boulmé
2021-05-28
7
-36
/
+98
*
splitting BTL by introducing BTLmatchRTL
Sylvain Boulmé
2021-05-28
6
-634
/
+614
*
fix some merge errors
Léo Gourdin
2021-05-28
3
-3
/
+4
*
Merge branch 'BTL_fsem' into BTL
Léo Gourdin
2021-05-28
5
-284
/
+840
|
\
|
*
most of the proof BTL.fsem -> BTL.cfgsem.
Sylvain Boulmé
2021-05-28
4
-46
/
+280
|
*
cleaning BTL_SEtheory
Sylvain Boulmé
2021-05-27
2
-190
/
+187
|
*
end of BTL_SEtheory w.r.t fsem
Sylvain Boulmé
2021-05-27
3
-182
/
+194
|
*
fix tr_sis definition
Sylvain Boulmé
2021-05-26
2
-81
/
+132
|
*
avancement roadmap
Sylvain Boulmé
2021-05-26
1
-11
/
+28
|
*
fix Builtin semantics
Sylvain Boulmé
2021-05-25
2
-37
/
+27
|
*
starting to experiment SE of fsem
Sylvain Boulmé
2021-05-25
2
-72
/
+232
|
*
improve fsem
Sylvain Boulmé
2021-05-21
1
-15
/
+30
|
*
update roadmap
Sylvain Boulmé
2021-05-20
1
-3
/
+10
|
*
defines fsem (aka functional semantics) of BTL
Sylvain Boulmé
2021-05-20
4
-19
/
+92
*
|
Improvements in scheduling and renumbering BTL code
Léo Gourdin
2021-05-28
5
-94
/
+65
*
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Léo Gourdin
2021-05-27
2
-349
/
+302
|
\
\
|
*
|
simplification of normRTL
Sylvain Boulmé
2021-05-25
1
-67
/
+27
|
*
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Sylvain Boulmé
2021-05-24
4
-21
/
+231
|
|
\
\
|
*
|
|
tiny simplifications in RTLtoBTLproof
Sylvain Boulmé
2021-05-24
2
-349
/
+342
*
|
|
|
[disabled checker] BTL Scheduling and Renumbering OK!
Léo Gourdin
2021-05-27
14
-181
/
+348
|
|
/
/
|
/
|
|
*
|
|
a draft frontend for prepass
Léo Gourdin
2021-05-24
4
-21
/
+231
|
/
/
*
|
Moving common tools, adding liveness input/output information to BTL generati...
Léo Gourdin
2021-05-24
7
-50
/
+32
*
|
splitting is_expand property with a weak version for conditions
Léo Gourdin
2021-05-23
2
-78
/
+117
*
|
Now supporting Bnop insertion in conditions
Léo Gourdin
2021-05-21
5
-139
/
+135
*
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Sylvain Boulmé
2021-05-20
13
-165
/
+550
|
\
\
|
|
/
|
/
|
|
*
working oracles (no renumber for now)
Léo Gourdin
2021-05-20
5
-79
/
+144
|
*
Changing to an opaq record in BTL info, this is a broken commit
Léo Gourdin
2021-05-20
7
-125
/
+141
|
*
Merge branch 'BTL' into BTL-translation
Léo Gourdin
2021-05-19
4
-10
/
+9
|
|
\
|
*
|
Adding a BTL record to help oracles
Léo Gourdin
2021-05-19
7
-165
/
+265
|
*
|
Grouping common RTL functions, printer improvement
Léo Gourdin
2021-05-19
4
-108
/
+26
|
*
|
first oracle seems ok
Léo Gourdin
2021-05-18
2
-11
/
+15
|
*
|
oracle simplification, BTL printer, and error msg spec
Léo Gourdin
2021-05-18
3
-97
/
+253
|
*
|
First draft of the RTL2BTL oracle
Léo Gourdin
2021-05-18
1
-4
/
+105
|
*
|
todos
Léo Gourdin
2021-05-18
1
-1
/
+1
|
*
|
preparing compiler passes and ml oracles
Léo Gourdin
2021-05-17
6
-12
/
+37
*
|
|
correction de l'idee de la Functional semantics
Sylvain Boulmé
2021-05-20
1
-26
/
+17
|
|
/
|
/
|
*
|
Merge branch 'kvx-work' into BTL
Léo Gourdin
2021-05-19
3
-8
/
+3
|
\
\
[next]