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
/
Asmblockgenproof0.v
Commit message (
Collapse
)
Author
Age
Files
Lines
*
move Asmblockgenproof0 from lib to mppa_k1c/
Sylvain Boulmé
2019-05-21
1
-0
/
+1134
|
|
|
|
This file is specific to our backend.
*
Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow that
Cyril SIX
2018-11-26
1
-1099
/
+0
|
*
Mise à jour vis à vis de CompCert 3.4
Cyril SIX
2018-11-21
1
-0
/
+18
|
*
Proved MBstore -> all instructions are proved
Cyril SIX
2018-11-08
1
-8
/
+0
|
*
MBop proved
Cyril SIX
2018-11-07
1
-7
/
+1
|
*
MBcond true proved (but a small change needs to be done to Asmblockgenproof1)
Cyril SIX
2018-11-06
1
-0
/
+15
|
*
Setting ep to false when the basicblock has a header. MBgoto done. ↵
Cyril SIX
2018-10-31
1
-0
/
+97
|
|
|
|
MBgetparam needs fix
*
MBtailcall proof
Cyril SIX
2018-10-29
1
-12
/
+18
|
*
Changing exec_straight to allow all instructions (prepare for MBtailcall proof)
Cyril SIX
2018-10-26
1
-17
/
+19
|
*
MBbuiltin proved
Cyril SIX
2018-10-26
1
-0
/
+68
|
*
Commencé à réintroduire du "ep" qui a du sens
Cyril SIX
2018-10-19
1
-16
/
+17
|
*
Avancement du schéma. A voir problème des traces
Cyril SIX
2018-10-10
1
-3
/
+15
|
*
Un peu d'avancement dans exec_straight_control et cie
Cyril SIX
2018-10-08
1
-12
/
+69
|
*
Removed the bundle attempt
Cyril SIX
2018-09-28
1
-2
/
+2
|
*
Preuve du internal_function (step_simulation)
Cyril SIX
2018-09-28
1
-7
/
+48
|
*
storeind_ptr_correct un peu d'avancée
Cyril SIX
2018-09-27
1
-3
/
+1
|
*
Avancement dans exec_straight_through
Cyril SIX
2018-09-27
1
-9
/
+51
|
*
Enlèvement du "no_builtin" condition; exec_control sur les option control; ↵
Cyril SIX
2018-09-26
1
-31
/
+76
|
|
|
|
exec_straight_blocks
*
AB: removing bregs
Cyril SIX
2018-09-26
1
-6
/
+8
|
*
MB2AB - un peu d'avancement sur internal function
Cyril SIX
2018-09-25
1
-2
/
+132
|
*
MB2AB - Proof of external function step
Cyril SIX
2018-09-25
1
-2
/
+57
|
*
MB2AB - Trois premières parties du lock-step
Cyril SIX
2018-09-21
1
-1
/
+301
|
*
return_address_exists -> done
Sylvain Boulmé
2018-09-20
1
-3
/
+1
|
*
avancement return_address
Sylvain Boulmé
2018-09-20
1
-45
/
+64
|
*
return_address suite
Sylvain Boulmé
2018-09-19
1
-3
/
+111
|
*
proof sketch for Asmgenproof.return_address_exists ?
Sylvain Boulmé
2018-09-19
1
-0
/
+4
|
*
premier jet Asmblockgenproof.return_address_offset
Sylvain Boulmé
2018-09-18
1
-0
/
+95