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
Commit message (
Expand
)
Author
Age
Files
Lines
*
fixing a potential inconsistency from unsafe_coerce
Sylvain Boulmé
2019-11-14
1
-5
/
+5
*
compatibility with OCaml 4.08
David Monniaux
2019-09-03
1
-1
/
+1
*
abstract_bb: few improvements while writing the paper
Sylvain Boulmé
2019-06-08
6
-251
/
+294
*
minor change in auxiliary lemma
Sylvain Boulmé
2019-05-28
1
-11
/
+21
*
simpler definition of reduce
Sylvain Boulmé
2019-05-28
2
-44
/
+118
*
slightly more efficient version
Sylvain Boulmé
2019-05-26
3
-40
/
+85
*
extending bblock_simu_test with rewriting
Sylvain Boulmé
2019-05-26
12
-1496
/
+1797
*
improving the scheduling verifier and its framework
Sylvain Boulmé
2019-05-16
2
-36
/
+149
*
abstractbb: support of removing useless computations
Sylvain Boulmé
2019-05-14
7
-299
/
+481
*
generalize bblock_equiv into bblock_simu (abstract_bb)
Sylvain Boulmé
2019-05-07
5
-51
/
+42
*
update from Impure Library
Sylvain Boulmé
2019-04-11
1
-20
/
+22
*
refactor for #92
Sylvain Boulmé
2019-04-11
2
-5
/
+31
*
moving iandb from ImpCore to ImpPrelude
Sylvain Boulmé
2019-04-08
2
-23
/
+18
*
Impure: improved iandb + struct_eq
Sylvain Boulmé
2019-04-01
2
-3
/
+11
*
renommage abstractbb: Name -> PReg
Sylvain Boulmé
2019-04-01
4
-7
/
+7
*
renommages abstract_bb
Sylvain Boulmé
2019-04-01
4
-132
/
+132
*
minor simpl
Sylvain Boulmé
2019-04-01
1
-8
/
+14
*
delete useless DepExample* files
Sylvain Boulmé
2019-04-01
4
-1051
/
+0
*
Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpass
David Monniaux
2019-03-28
1
-0
/
+18
|
\
|
*
dealing with permutations
Sylvain Boulmé
2019-03-27
1
-0
/
+18
*
|
remove a FAILWITH that forbids some debugging information to be printed
Sylvain Boulmé
2019-03-19
1
-3
/
+3
|
/
*
Fix for CompCert 3.5
Cyril SIX
2019-03-13
1
-0
/
+1
*
quick fix of equalities issues
Sylvain Boulmé
2019-03-05
1
-0
/
+4
*
fix extraction of ImpConfig
Sylvain Boulmé
2019-03-05
1
-2
/
+5
*
compilation of ImpIOOracles
Sylvain Boulmé
2019-03-05
2
-4
/
+8
*
remove cumbersome dependency on genv in bblock_eq_test
Sylvain Boulmé
2019-03-05
3
-27
/
+27
*
(Unsafe) coercion of ??bool into bool
Sylvain Boulmé
2019-03-02
1
-2
/
+2
*
[BROKEN] trying to generalize Sylvain's abstract bb to include a genv.
Cyril SIX
2019-02-20
7
-87
/
+133
*
Added AbstractBasicBlock files to the Coq build process
Cyril SIX
2019-02-13
25
-0
/
+4692