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
/
mppa_k1c
/
abstractbb
/
AbstractBasicBlocksDef.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
k1c -> kvx changes
David Monniaux
2020-05-26
1
-452
/
+0
*
Adding copyrights
Cyril SIX
2020-05-04
1
-0
/
+14
*
removing warnings on hints in core
Sylvain Boulmé
2020-03-07
1
-1
/
+1
*
minor change in auxiliary lemma
Sylvain Boulmé
2019-05-28
1
-11
/
+21
*
simpler definition of reduce
Sylvain Boulmé
2019-05-28
1
-29
/
+94
*
slightly more efficient version
Sylvain Boulmé
2019-05-26
1
-5
/
+5
*
extending bblock_simu_test with rewriting
Sylvain Boulmé
2019-05-26
1
-10
/
+120
*
generalize bblock_equiv into bblock_simu (abstract_bb)
Sylvain Boulmé
2019-05-07
1
-11
/
+11
*
refactor for #92
Sylvain Boulmé
2019-04-11
1
-1
/
+27
*
renommage abstractbb: Name -> PReg
Sylvain Boulmé
2019-04-01
1
-3
/
+3
*
renommages abstract_bb
Sylvain Boulmé
2019-04-01
1
-12
/
+12
*
remove cumbersome dependency on genv in bblock_eq_test
Sylvain Boulmé
2019-03-05
1
-0
/
+5
*
[BROKEN] trying to generalize Sylvain's abstract bb to include a genv.
Cyril SIX
2019-02-20
1
-2
/
+10
*
Added AbstractBasicBlock files to the Coq build process
Cyril SIX
2019-02-13
1
-0
/
+214