compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	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; ↵	Cyril SIX	2018-09-26	1	-12/+25
\| \| \| \|	exec_straight_blocks
*	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Asmblock.v: - Rajout de "header" dans wf_bblock - Remplacer "code" par "bblocks". Pour la suite, je trouve plus clair de manipuler des bblocks, plutôt qu'un "code constitué de bblocks". ça permet de minimiser les modifications dans Asmblockgen.v - fn_code --> fn_blocks . fn_code ne devrait pas être utilisé dans le code OCaml de toute façon (vu la translation Asmblock -> Asm) - Rajout d'un type instruction qui regroupe les basic et les control ; facilite certaines définitions Asmblockgen.v: - Copie conforme de Asmgen.v, avec quelques changements (pas fini). Ce vers quoi je m'oriente : garder les fonctions existantes de génération de code ; on leur donne à manger la liste de basics de Machblock. On traduit le exit (qui peut spiller sur la liste de basics déjà traduite), et on met la dernière instruction de la trad du exit (qui doit être un control) dans le exit du bblock. - Pour le prologue : chaque instruction rajoutée "à la main" est dans son propre bblock. Voir la notation ::b pour le faire. A terme, il devrait y avoir moyen "d'accumuler" l'instruction au code généré ; pour l'instant je préfère ne pas compliquer la génération.
*	deplacement allocframe/freeframe/loadsymbol	Sylvain Boulmé	2018-09-06	1	-41/+37
\| \| \| \|	dans instructions basiques des blocs.
*	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
	mixed between Machblock style and Asm...