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
Commit message (
Expand
)
Author
Age
Files
Lines
*
Branching stub scheduler
Cyril SIX
2020-05-28
2
-9
/
+44
*
Removing debug
Cyril SIX
2020-05-27
1
-3
/
+0
*
FIX: was making too big paths (including call and builtins in paths)
Cyril SIX
2020-05-27
1
-1
/
+4
*
Using Sylvain's suggestion instead
Cyril SIX
2020-05-26
1
-23
/
+55
*
Making our own Kildall variant
Cyril SIX
2020-05-26
1
-47
/
+85
*
Attempt to modify the transfer function
Cyril SIX
2020-05-26
1
-1
/
+39
*
The backend/Liveness.v is not enough
Cyril SIX
2020-05-26
1
-6
/
+17
*
First try for build_path_map
Cyril SIX
2020-05-25
1
-2
/
+166
*
Adding stub RTLpathLivegenaux.ml
Cyril SIX
2020-05-25
2
-0
/
+6
*
RTL -> RTLpath -> RTL
Cyril SIX
2020-05-20
1
-1
/
+70
*
Revert "Modifying RTLpath in order to allow for stopping at Icond"
Cyril SIX
2020-05-20
1
-23
/
+11
*
Modifying RTLpath in order to allow for stopping at Icond
Cyril SIX
2020-05-20
1
-11
/
+23
*
No need to change default_succ : we keep ifnot as default, and adjust the pat...
Cyril SIX
2020-05-20
1
-2
/
+0
*
Admitting the rest
Cyril SIX
2020-05-20
2
-7
/
+7
*
Stailcall
Cyril SIX
2020-05-20
1
-5
/
+21
*
Proof of sisteps_correct_false
Cyril SIX
2020-05-19
1
-8
/
+31
*
sistep_correct proved completely
Cyril SIX
2020-05-19
1
-21
/
+16
*
Avancement on sistep_correct for load
Cyril SIX
2020-05-19
1
-4
/
+22
*
Progress on load_notrap_value in symbolic execution
Cyril SIX
2020-04-30
1
-12
/
+27
*
Progression on LOAD sistep_correct
Cyril SIX
2020-04-30
1
-3
/
+30
*
Back to a proven sistep_correct (except for the LOAD case)
Cyril SIX
2020-04-30
1
-19
/
+26
*
Proof of sistep_preserves_sabort
Cyril SIX
2020-04-29
1
-19
/
+63
*
Complete proof of ssem_exclude_sabort
Cyril SIX
2020-04-29
1
-5
/
+8
*
ssem_exit_fallthrough_upto_exit finally done - it was very simple actually
Cyril SIX
2020-04-29
1
-64
/
+7
*
The lemmas i was basing my theorems on are actually wrong..
Cyril SIX
2020-04-29
1
-48
/
+39
*
Proving admitted ssem_exit_fallthrough_upto_exit -> need to prove is_tail_exists
Cyril SIX
2020-04-28
1
-30
/
+38
*
Proof of ssem_exit_exclude_sabort - on avance !
Cyril SIX
2020-04-28
1
-41
/
+11
*
Cutting ssem_exits into two pieces + advancing some proofs
Cyril SIX
2020-04-27
1
-130
/
+248
*
no: the simpler fix is too simple...
Sylvain Boulmé
2020-04-25
1
-22
/
+14
*
a simpler fix ?
Sylvain Boulmé
2020-04-25
1
-2
/
+18
*
fixing sabort_exits ?
Sylvain Boulmé
2020-04-24
1
-1
/
+16
*
Reverting change to sistate
Cyril SIX
2020-04-24
1
-39
/
+7
*
[BROKEN] Added wf predicate sistate - simatch_exclude_abort proven, need to m...
Cyril SIX
2020-04-23
1
-77
/
+121
*
Finished renaming
Cyril SIX
2020-04-23
2
-337
/
+339
*
Started general renaming for clearer and more understandable code
Cyril SIX
2020-04-22
3
-250
/
+243
*
list_val_inj --> list_sval_inj
Cyril SIX
2020-04-22
1
-8
/
+8
*
Trying to cut sem_istate_exclude_abort into lemmas
Cyril SIX
2020-04-22
1
-8
/
+68
*
Added and cleaned some comments on RTLpath.v
Cyril SIX
2020-04-21
1
-1
/
+8
*
notrap cases
David Monniaux
2020-04-15
1
-3
/
+5
*
Some progress on notrap load
Cyril SIX
2020-04-15
3
-23
/
+61
*
Fixing the merge. Needs to add notrap load semantics + prove other admitted s...
Cyril SIX
2020-04-10
3
-61
/
+71
*
[BROKEN] Merge branch 'mppa-work' into mppa-RTLpathSE
Cyril SIX
2020-04-10
31
-770
/
+1526
|
\
|
*
Fix cutrewrite deprecated
Cyril SIX
2020-04-01
1
-3
/
+4
|
*
proof clarification
David Monniaux
2020-03-20
1
-3
/
+5
|
*
more understandabe proofs
David Monniaux
2020-03-20
1
-38
/
+38
|
*
progress in RA invariants
David Monniaux
2020-03-20
1
-23
/
+24
|
*
Duplicate: getting rid of the annoying exception-based code
Cyril SIX
2020-03-09
1
-7
/
+2
|
*
removing more coq8.10 warnings
Sylvain Boulmé
2020-03-09
4
-2
/
+10
|
*
removing some coqc 8.10 warnings
Sylvain Boulmé
2020-03-09
1
-4
/
+4
|
*
removing warnings on hints in core
Sylvain Boulmé
2020-03-07
11
-42
/
+39
[next]