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 (
Expand
)
Author
Age
Files
Lines
*
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
*
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
*
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 s...
Cyril SIX
2020-04-10
3
-61
/
+71
*
[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
|
|
|
*
Double rounding error in int64->float32 conversions on PowerPC and ARM
Xavier Leroy
2020-03-30
4
-24
/
+22
|
|
|
*
Add a test for int64 -> float32 conversion
Xavier Leroy
2020-03-30
2
-39
/
+838
|
|
|
*
Explicit error messages for ill-formed section attributes (#232)
Bernhard Schommer
2020-03-29
3
-12
/
+25
|
|
*
|
-fduplicate -1 really desactivates the pass in Coq now
Cyril SIX
2020-04-01
3
-7
/
+8
|
|
*
|
Fix cutrewrite deprecated
Cyril SIX
2020-04-01
1
-3
/
+4
|
|
*
|
Removing 8.8.* versions of coq in configure
Cyril SIX
2020-04-01
1
-1
/
+1
|
|
*
|
do not run check-admitted always
David Monniaux
2020-03-31
1
-0
/
+8
|
|
*
|
move check-admitted elsewhere
David Monniaux
2020-03-31
1
-2
/
+6
|
|
*
|
forgot image
David Monniaux
2020-03-31
1
-0
/
+1
[next]