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

	Commit message (Expand)	Author	Age	Files	Lines
...
*	step_simulation_bblock' is back online, using exec_body instead of exec_straight	Cyril SIX	2018-10-16	1	-19/+74
*	transl_blocks de nouveau prouvé + Ltac exploreInst	Cyril SIX	2018-10-16	1	-20/+73
*	Réintroduction du Pnop, que si pas de body et d'exit. Réécriture du transl...	Cyril SIX	2018-10-15	1	-68/+71
*	Disjonction des cas MB.body bb = nil ou non	Cyril SIX	2018-10-12	1	-5/+7
*	Stuck on proving step_simu_body	Cyril SIX	2018-10-12	1	-1588/+1622
*	Separating the case of MBbuiltin from the rest	Cyril SIX	2018-10-12	1	-16/+24
*	Avancement du schéma. A voir problème des traces	Cyril SIX	2018-10-10	1	-243/+71
*	Preuve de MBcall et du exit=None dans le step_simu_control	Cyril SIX	2018-10-10	1	-31/+113
*	Beaucoup de quincaillerie avec les transl_blocks, travail en cours	Cyril SIX	2018-10-09	1	-23/+116
*	Un peu d'avancement dans exec_straight_control et cie	Cyril SIX	2018-10-08	1	-32/+105
*	Fini le cas du step_simu_control où il n'y a pas de exit	Cyril SIX	2018-10-04	1	-20/+50
*	Schéma de simulation + les Pnop sont maintenant implicites	Cyril SIX	2018-10-03	1	-15/+88
*	match_codestate et match_asmblock	Cyril SIX	2018-10-02	1	-33/+142
*	Separation de step_simulation_bblock en step_simu_control et step_simu_basic	Cyril SIX	2018-10-01	1	-5/+62
*	Preuve du internal_function (step_simulation)	Cyril SIX	2018-09-28	1	-23/+35
*	storeind_ptr_correct un peu d'avancée	Cyril SIX	2018-09-27	1	-4/+3
*	Enlèvement du "no_builtin" condition; exec_control sur les option control; e...	Cyril SIX	2018-09-26	1	-2/+2
*	AB: removing bregs	Cyril SIX	2018-09-26	1	-1/+1
*	MB2AB - un peu d'avancement sur internal function	Cyril SIX	2018-09-25	1	-4/+76
*	MB2AB - Proof of external function step	Cyril SIX	2018-09-25	1	-4/+21
*	relecture	Sylvain Boulmé	2018-09-24	1	-12/+1
*	MB2AB - changement du lock-step en star, cas du Returnstate fait	Cyril SIX	2018-09-21	1	-10/+27
*	MB2AB - Trois premières parties du lock-step	Cyril SIX	2018-09-21	1	-16/+21
*	return_address_exists -> done	Sylvain Boulmé	2018-09-20	1	-15/+12
*	return_address suite	Sylvain Boulmé	2018-09-19	1	-3/+7
*	premier jet Asmblockgenproof.return_address_offset	Sylvain Boulmé	2018-09-18	1	-2/+2
*	Asmblock -> Asm presque fini.. erreur sur driver/Compiler.v	Cyril SIX	2018-09-06	1	-2/+1
*	Asmblock: Adding forward_simulation and determinism as axioms	Cyril SIX	2018-09-06	1	-0/+1124