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
/
kvx
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
Cyril SIX
2020-12-01
1
-1
/
+0
|
\
|
*
pointer_eq copied
David Monniaux
2020-11-25
1
-0
/
+20
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-11-24
2
-12
/
+22
|
\
|
|
*
correction bug #223 sur KVX
David Monniaux
2020-11-23
2
-12
/
+22
*
|
new OpWeights
David Monniaux
2020-10-22
2
-0
/
+25
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-10-18
2
-7
/
+16
|
\
|
|
*
centralize if_same
David Monniaux
2020-10-09
1
-6
/
+0
|
*
do not synthesize select if both operands are identical
David Monniaux
2020-10-09
2
-7
/
+22
*
|
update op_valid_pointer_eq proof on the KVX
Sylvain Boulmé
2020-10-17
1
-22
/
+4
*
|
fixing the move of the verified prepass scheduler into scheduling/ directory
Sylvain Boulmé
2020-10-17
1
-872
/
+0
*
|
Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verif
Cyril SIX
2020-10-16
55
-11464
/
+859
|
\
\
|
*
|
so that all architectures compile
David Monniaux
2020-10-02
1
-0
/
+1
|
*
|
non pipelined units = none on KVX
David Monniaux
2020-09-30
1
-1
/
+3
|
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-09-29
23
-769
/
+765
|
|
\
|
|
|
*
simpl -> cbn
David Monniaux
2020-09-29
23
-793
/
+789
|
*
|
Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepass
David Monniaux
2020-09-22
1
-14
/
+0
|
|
\
\
|
|
*
|
reflect changes
David Monniaux
2020-09-22
1
-14
/
+0
|
*
|
|
Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepass
David Monniaux
2020-09-21
2
-272
/
+1
|
|
\
|
|
|
|
*
|
moved some "total" value domain functions to a central location
David Monniaux
2020-09-21
1
-271
/
+0
|
|
|
/
|
|
*
use scheduler_by_name
David Monniaux
2020-09-10
3
-9
/
+11
|
*
|
just missing OpWeights for AARCH64
David Monniaux
2020-09-16
14
-9446
/
+0
|
*
|
starting to move common files
David Monniaux
2020-09-16
16
-1651
/
+0
|
*
|
Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-...
David Monniaux
2020-09-10
12
-222
/
+230
|
|
\
\
|
|
*
|
Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash...
David Monniaux
2020-09-05
6
-75
/
+117
|
|
|
\
|
|
|
|
*
fix issue 198 (incorrect reservation table for multiply-add)
David Monniaux
2020-09-02
1
-5
/
+5
|
|
|
*
"nop" is not even printed out and thus uses no resources
David Monniaux
2020-09-01
1
-13
/
+21
|
|
|
*
clean solution to close channels
David Monniaux
2020-08-31
1
-21
/
+24
|
|
|
*
fix problem with some file descriptors possibly never getting closed
David Monniaux
2020-08-31
1
-4
/
+10
|
|
|
*
links to the impure library on github
Sylvain Boulmé
2020-07-31
1
-1
/
+2
|
|
|
*
Improving Coqdoc on abstractbb
Sylvain Boulmé
2020-07-31
4
-46
/
+71
|
*
|
|
use with_destructor
David Monniaux
2020-09-10
2
-20
/
+29
*
|
|
|
removing useless opt_simu
Sylvain Boulmé
2020-10-13
3
-36
/
+25
*
|
|
|
refactoring of RTLpathSE_impl.v (split with _simu_specs)
Sylvain Boulmé
2020-10-13
5
-3911
/
+2086
*
|
|
|
remove the last tiny issue!
Sylvain Boulmé
2020-10-12
1
-10
/
+3
*
|
|
|
simpl hsstate_simu_core_correct
Sylvain Boulmé
2020-10-12
1
-3
/
+1
*
|
|
|
fix one issue by generalizing RTLpathSE_theory.sstate_simu
Sylvain Boulmé
2020-10-12
2
-9
/
+18
*
|
|
|
move issue from hsexec_correct to hsstate_simu_core_correct
Sylvain Boulmé
2020-10-12
1
-14
/
+19
*
|
|
|
most of the proof is done ! two (small ?) issues remain...
Sylvain Boulmé
2020-10-12
1
-30
/
+83
*
|
|
|
oops: forget to save before compile/commit/push
Sylvain Boulmé
2020-10-12
1
-2
/
+5
*
|
|
|
end of merge with Cyril's proof
Sylvain Boulmé
2020-10-12
2
-59
/
+227
*
|
|
|
starting to merge with Cyril's proof
Sylvain Boulmé
2020-10-11
1
-48
/
+773
*
|
|
|
hconsing: full proof of hsiexec_path_correct
Sylvain Boulmé
2020-10-10
2
-42
/
+71
*
|
|
|
progress on hslocal_set_sreg_correct
Sylvain Boulmé
2020-10-10
1
-37
/
+53
*
|
|
|
progress on hsexec_inst_correct_dyn
Sylvain Boulmé
2020-10-10
1
-39
/
+140
*
|
|
|
hconsing: red_PTree_set_correct
Sylvain Boulmé
2020-10-09
1
-0
/
+11
*
|
|
|
hconsing: root_happly_correct + simplify_correct DONE
Sylvain Boulmé
2020-10-09
4
-15
/
+145
*
|
|
|
prove the kvx-test-prepass fix (commit 0e4186b8f)
Sylvain Boulmé
2020-10-08
1
-14
/
+58
*
|
|
|
Merge branch 'mppa-RTLpathSE-verif_Op_mem-irrel' into mppa-RTLpathSE-xverif
Sylvain Boulmé
2020-10-08
1
-30
/
+29
|
\
\
\
\
|
*
|
|
|
prove the trick of simplify (as implemented in RTLpathSE_impl_junk)
Sylvain Boulmé
2020-08-27
1
-18
/
+6
|
*
|
|
|
prove that Mem.valid is preserved by symbolic execution of RTLpath
Sylvain Boulmé
2020-08-27
1
-12
/
+22
[next]