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
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Branching stub scheduler
Cyril SIX
2020-05-28
3
-14
/
+55
|
*
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
3
-1
/
+8
|
*
RTL -> RTLpath -> RTL
Cyril SIX
2020-05-20
2
-3
/
+86
|
*
Revert "Modifying RTLpath in order to allow for stopping at Icond"
Cyril SIX
2020-05-20
1
-23
/
+11
|
|
|
|
This reverts commit b6a6e7b783cc59f2efd2fc2470f6676d88d3f58f.
*
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 ↵
Cyril SIX
2020-05-20
1
-2
/
+0
|
|
|
|
path number if we want to stop earlier
*
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 ↵
Cyril SIX
2020-04-23
1
-77
/
+121
|
|
|
|
modify some functions
*
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
|
*
allow Coq 8.11.1
David Monniaux
2020-04-13
1
-1
/
+1
|
*
Fixing the merge. Needs to add notrap load semantics + prove other admitted ↵
Cyril SIX
2020-04-10
3
-61
/
+71
|
|
|
|
stuff
*
[BROKEN] Merge branch 'mppa-work' into mppa-RTLpathSE
Cyril SIX
2020-04-10
272
-3107
/
+14919
|
\
|
*
Stopping traces at join points
Cyril SIX
2020-04-01
1
-2
/
+25
|
|
|
*
Merge remote-tracking branch 'origin/mppa-work' into mppa-branch-info
Cyril SIX
2020-04-01
36
-477
/
+2024
|
|
\
|
|
*
Fixing packedstruct issue
v3.7_mppa_2020-04-01
Cyril SIX
2020-04-01
2
-15
/
+15
|
|
|
|
|
*
Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-work
Cyril SIX
2020-04-01
12
-80
/
+926
|
|
|
\
|
|
|
*
Updates for release 3.7
v3.7
Xavier Leroy
2020-03-31
1
-1
/
+1
|
|
|
|
|
|
|
*
Updates for release 3.7
Xavier Leroy
2020-03-31
2
-1
/
+6
|
|
|
|
|
|
|
*
Update Changelog
Xavier Leroy
2020-03-31
1
-3
/
+34
|
|
|
|
[next]