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
/
Asmblock.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Adding a predicate that a builtin must be alone in its basicblock
Cyril SIX
2019-01-23
1
-79
/
+139
*
Added sxwd and zxwd support
Cyril SIX
2019-01-22
1
-4
/
+4
*
Generalizing PostpassScheduling to include bblock splitting
Cyril SIX
2018-12-05
1
-4
/
+8
*
Moving size_blocks from Asmblockgen to Asmblock
Cyril SIX
2018-12-05
1
-0
/
+8
*
Changed ABI to match GCC - interoperability not tested yet
Cyril SIX
2018-11-23
1
-12
/
+13
*
Mise à jour vis à vis de CompCert 3.4
Cyril SIX
2018-11-21
1
-1
/
+11
*
Déterminisme prouvé -> Tout est prouvé
Cyril SIX
2018-11-08
1
-1
/
+59
*
Proved non_empty_bblock_refl (was Admitted)
Cyril SIX
2018-11-08
1
-4
/
+4
*
Changing exec_straight to allow all instructions (prepare for MBtailcall proof)
Cyril SIX
2018-10-26
1
-0
/
+35
*
Adding "proof irrelevance" to bblocks
Cyril SIX
2018-10-25
1
-15
/
+49
*
MBsetstack done!
Cyril SIX
2018-10-24
1
-2
/
+2
*
step_simulation_bblock is back!
Cyril SIX
2018-10-24
1
-1
/
+1
*
ajoute un axiom a virer plus tard
Sylvain Boulmé
2018-10-23
1
-1
/
+7
*
Un peu d'avancement dans exec_straight_control et cie
Cyril SIX
2018-10-08
1
-13
/
+12
*
Fini le cas du step_simu_control où il n'y a pas de exit
Cyril SIX
2018-10-04
1
-14
/
+9
*
Schéma de simulation + les Pnop sont maintenant implicites
Cyril SIX
2018-10-03
1
-8
/
+22
*
Removed the bundle attempt
Cyril SIX
2018-09-28
1
-47
/
+7
*
Enlèvement du "no_builtin" condition; exec_control sur les option control; e...
Cyril SIX
2018-09-26
1
-12
/
+25
*
AB: removing bregs
Cyril SIX
2018-09-26
1
-68
/
+37
*
MB2AB - un peu d'avancement sur internal function
Cyril SIX
2018-09-25
1
-8
/
+6
*
MB2AB - Proof of external function step
Cyril SIX
2018-09-25
1
-7
/
+7
*
relecture
Sylvain Boulmé
2018-09-24
1
-1
/
+3
*
a few stubs for bundling
Sylvain Boulmé
2018-09-24
1
-194
/
+0
*
one step toward "bundle_step"
Sylvain Boulmé
2018-09-24
1
-6
/
+55
*
Asmblock -> Asm presque fini.. erreur sur driver/Compiler.v
Cyril SIX
2018-09-06
1
-249
/
+259
*
Asmblockgen: Added Pnop and Program Definitions
Cyril SIX
2018-09-06
1
-38
/
+7
*
Example of Program use...
Sylvain Boulmé
2018-09-06
1
-0
/
+16
*
Asmblock: Adding forward_simulation and determinism as axioms
Cyril SIX
2018-09-06
1
-0
/
+2
*
Asmblockgen.v finished (no proof yet)
Cyril SIX
2018-09-06
1
-15
/
+46
*
Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléter
Cyril SIX
2018-09-06
1
-12
/
+42
*
deplacement allocframe/freeframe/loadsymbol
Sylvain Boulmé
2018-09-06
1
-41
/
+37
*
Name changing + introducing Pbuiltin (alone in a block)
Cyril SIX
2018-09-06
1
-91
/
+67
*
Some renaming on asmblock
Cyril SIX
2018-09-06
1
-11
/
+11
*
add comments (TODO/FIXME)
Sylvain Boulmé
2018-09-06
1
-11
/
+28
*
notation change
Sylvain Boulmé
2018-09-06
1
-21
/
+21
*
a version of Asmblock syntax and semantics
Sylvain Boulmé
2018-09-06
1
-0
/
+1376