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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8	David Monniaux	2020-11-18	1	-1/+1
\|\
\| *	Transform non-recursive Fixpoint into Definition	Xavier Leroy	2020-06-21	1	-1/+1
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version.
* \|	more proofs going through	David Monniaux	2019-09-05	1	-1/+1
\|/
*	Support for 64-bit architectures: generic support	Xavier Leroy	2016-10-01	1	-1/+1
\| \| \| \| \| \| \| \| \| \| \|	- Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
*	Update the back-end proofs to the new linking framework.	Xavier Leroy	2016-03-06	1	-12/+3
\|
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-4/+4
\|
*	Track the locations of local variables using EF_debug annotations.	Xavier Leroy	2015-08-23	1	-0/+378
	SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known.