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

	Commit message (Collapse)	Author	Age	Files	Lines
*	[Cherry picking] 01ade46b340267d8782c413f6bd5a3cff13ef0a6	Léo Gourdin	2021-12-06	1	-26/+26
\| \| \| \|	starting a new index-verimag.html on BTL doc
*	cleaner symbolic semantic of load traps	Sylvain Boulmé	2021-10-25	1	-12/+10
\|
*	[MERGE] BTL into kvx-work (replacing RTLpath)	Léo Gourdin	2021-09-01	1	-2/+2
\|
*	non trapping loads	Léo Gourdin	2021-07-23	1	-17/+27
\|
*	add hid in BTL_SEtheory: this avoids duplication of types (and should not be ↵	Sylvain Boulmé	2021-06-11	1	-127/+142
\| \| \| \|	harmful)
*	remove history	Sylvain Boulmé	2021-06-10	1	-8/+10
\|
*	fix sstate_simu	Sylvain Boulmé	2021-06-09	1	-1/+17
\|
*	valid_pointer_preserv dans BTL_SEtheory => opportunites de grosses ↵	Sylvain Boulmé	2021-06-09	1	-21/+29
\| \| \| \|	simplifications (à venir )
*	avancement ref de l'exe symbolique	Sylvain Boulmé	2021-06-07	1	-7/+4
\|
*	starting refinement of symbolic execution	Sylvain Boulmé	2021-06-04	1	-9/+9
\|
*	progress in BTL_SEsimuref	Sylvain Boulmé	2021-06-04	1	-23/+11
\|
*	progress in BTL_SEsimuref	Sylvain Boulmé	2021-06-03	1	-31/+54
\|
*	minor renaming	Sylvain Boulmé	2021-06-02	1	-9/+9
\|
*	fix the definition of [symbolic_simu] in BTL_SEtheory	Sylvain Boulmé	2021-06-02	1	-64/+243
\|
*	the current "high-level" specification of the simulation test will not work !	Sylvain Boulmé	2021-06-02	1	-10/+48
\|
*	starting BTL_SEsimuref	Sylvain Boulmé	2021-06-01	1	-99/+1
\|
*	remove dupmap from BTL_Scheduler !	Sylvain Boulmé	2021-05-28	1	-14/+10
\|
*	archi pour la verif du scheduler	Sylvain Boulmé	2021-05-28	1	-11/+13
\|
*	fix some merge errors	Léo Gourdin	2021-05-28	1	-1/+1
\|
*	Merge branch 'BTL_fsem' into BTL	Léo Gourdin	2021-05-28	1	-246/+295
\|\
\| *	most of the proof BTL.fsem -> BTL.cfgsem.	Sylvain Boulmé	2021-05-28	1	-1/+1
\| \|
\| *	cleaning BTL_SEtheory	Sylvain Boulmé	2021-05-27	1	-190/+114
\| \|
\| *	end of BTL_SEtheory w.r.t fsem	Sylvain Boulmé	2021-05-27	1	-162/+169
\| \|
\| *	fix tr_sis definition	Sylvain Boulmé	2021-05-26	1	-57/+90
\| \|
\| *	fix Builtin semantics	Sylvain Boulmé	2021-05-25	1	-27/+3
\| \|
\| *	starting to experiment SE of fsem	Sylvain Boulmé	2021-05-25	1	-55/+158
\| \|
\| *	defines fsem (aka functional semantics) of BTL	Sylvain Boulmé	2021-05-20	1	-6/+12
\| \|
* \|	Changing to an opaq record in BTL info, this is a broken commit	Léo Gourdin	2021-05-20	1	-7/+7
\| \|
* \|	Adding a BTL record to help oracles	Léo Gourdin	2021-05-19	1	-11/+11
\|/
*	better autodestruct ?	Sylvain Boulmé	2021-05-11	1	-16/+0
\|
*	prove sexec_exact	Sylvain Boulmé	2021-05-11	1	-11/+323
\|
*	sexec: renommage Sdead -> Sabort + simplification de sexec_correct	Sylvain Boulmé	2021-05-08	1	-57/+21
\|
*	start a model of symbolic execution in Continuation-Passing-Style	Sylvain Boulmé	2021-05-07	1	-18/+233
\|
*	fix SymbValPreserved section	Sylvain Boulmé	2021-05-07	1	-1/+98
\|
*	refactorisation + 1ere version de sstate	Sylvain Boulmé	2021-05-06	1	-1461/+169
\|
*	init BTL_SEtheory (by copy/paste from RTLpathSE_theory)	Sylvain Boulmé	2021-05-06	1	-0/+1831