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
*
transf fct correct in BTL scheduler proof
Léo Gourdin
2021-06-20
1
-5
/
+5
*
finish main proof
Léo Gourdin
2021-06-19
1
-18
/
+128
*
lemma on eqregs?
Léo Gourdin
2021-06-18
2
-14
/
+7
*
finish RTLtoBTL proof
Léo Gourdin
2021-06-18
1
-2
/
+18
*
End of main scheduling proof
Léo Gourdin
2021-06-18
3
-59
/
+90
*
some advance, new section to simplify context from symbolic exec
Léo Gourdin
2021-06-17
3
-66
/
+151
*
some advance in sched proof
Léo Gourdin
2021-06-15
1
-24
/
+92
*
Preparation for scheduling proof, main lemmas ok
Léo Gourdin
2021-06-14
4
-16
/
+41
*
begin scheduler BTL proof
Léo Gourdin
2021-06-14
2
-5
/
+142
*
stub match_states
Sylvain Boulmé
2021-06-11
1
-1
/
+3
*
add hid in BTL_SEtheory: this avoids duplication of types (and should not be ...
Sylvain Boulmé
2021-06-11
2
-150
/
+157
*
Roadmap: precision sur le cout de verification des superblocks
Sylvain Boulmé
2021-06-11
1
-2
/
+9
*
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Sylvain Boulmé
2021-06-11
4
-39
/
+43
|
\
|
*
Merge branch 'kvx-work' into BTL
Léo Gourdin
2021-06-10
4
-39
/
+43
|
|
\
|
|
*
Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1
Cyril SIX
2021-06-01
7
-31
/
+24
|
|
|
\
|
|
*
|
replacing omega with lia in some file
Léo Gourdin
2021-03-29
4
-39
/
+43
*
|
|
|
proving the remaining lemma for sexec_rec_okpreserv
Sylvain Boulmé
2021-06-11
1
-123
/
+162
|
/
/
/
*
|
|
theorem rexec_simu_correct
Sylvain Boulmé
2021-06-10
1
-25
/
+111
*
|
|
fix rst_simu_correct
Sylvain Boulmé
2021-06-10
1
-27
/
+21
*
|
|
remove history
Sylvain Boulmé
2021-06-10
2
-196
/
+121
*
|
|
fix sstate_simu
Sylvain Boulmé
2021-06-09
2
-32
/
+35
*
|
|
valid_pointer_preserv dans BTL_SEtheory => opportunites de *grosses* simplifi...
Sylvain Boulmé
2021-06-09
2
-87
/
+42
*
|
|
generalize nested
Sylvain Boulmé
2021-06-09
1
-71
/
+74
*
|
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Sylvain Boulmé
2021-06-08
1
-28
/
+172
|
\
\
\
|
*
|
|
End of liveness proof
Léo Gourdin
2021-06-07
1
-54
/
+45
|
*
|
|
ugly complete version of liveness proof (I will clean in next commits)
Léo Gourdin
2021-06-07
1
-34
/
+40
|
*
|
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Léo Gourdin
2021-06-07
3
-27
/
+351
|
|
\
\
\
|
*
|
|
|
advance for tr_input proof
Léo Gourdin
2021-06-07
1
-24
/
+171
*
|
|
|
|
preuve de rexec_rec_correct via les notions history/histOK
Sylvain Boulmé
2021-06-08
1
-41
/
+251
|
|
/
/
/
|
/
|
|
|
*
|
|
|
avancement ref de l'exe symbolique
Sylvain Boulmé
2021-06-07
2
-26
/
+306
*
|
|
|
m
Sylvain Boulmé
2021-06-06
1
-1
/
+3
*
|
|
|
IDEE pour la STRENGTH-REDUCTION
Sylvain Boulmé
2021-06-06
1
-1
/
+43
|
/
/
/
*
|
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Léo Gourdin
2021-06-04
2
-12
/
+115
|
\
\
\
|
*
|
|
starting refinement of symbolic execution
Sylvain Boulmé
2021-06-04
2
-12
/
+115
*
|
|
|
preparation and starting final lemma
Léo Gourdin
2021-06-04
1
-21
/
+100
|
/
/
/
*
|
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Léo Gourdin
2021-06-04
3
-35
/
+77
|
\
\
\
|
*
|
|
progress in BTL_SEsimuref
Sylvain Boulmé
2021-06-04
3
-35
/
+77
*
|
|
|
Some advance in Liveness lemmas
Léo Gourdin
2021-06-04
1
-71
/
+138
|
/
/
/
*
|
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Léo Gourdin
2021-06-03
2
-109
/
+112
|
\
\
\
|
*
\
\
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Sylvain Boulmé
2021-06-03
1
-21
/
+112
|
|
\
\
\
|
*
|
|
|
progress in BTL_SEsimuref
Sylvain Boulmé
2021-06-03
2
-109
/
+112
*
|
|
|
|
update a more general version of the liveness checker
Léo Gourdin
2021-06-03
1
-93
/
+118
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Léo Gourdin
2021-06-02
2
-176
/
+255
|
\
|
|
|
|
*
|
|
minor renaming
Sylvain Boulmé
2021-06-02
1
-9
/
+9
|
*
|
|
fix the definition of [symbolic_simu] in BTL_SEtheory
Sylvain Boulmé
2021-06-02
2
-172
/
+251
*
|
|
|
lemmas on entrypoint, tr_inputs, eqlive_regs, ...
Léo Gourdin
2021-06-02
1
-21
/
+112
|
/
/
/
*
|
|
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...
Léo Gourdin
2021-06-02
3
-110
/
+416
|
\
\
\
|
*
|
|
the current "high-level" specification of the simulation test will not work !
Sylvain Boulmé
2021-06-02
3
-37
/
+124
|
*
|
|
starting BTL_SEsimuref
Sylvain Boulmé
2021-06-01
2
-99
/
+318
*
|
|
|
some advance in main liveness lemmas
Léo Gourdin
2021-06-02
1
-28
/
+68
|
/
/
/
[next]