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

	Commit message (Collapse)	Author	Age	Files	Lines
*	rm unneeded open statements in ML	David Monniaux	2020-11-19	1	-3/+0
\|
*	Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8	David Monniaux	2020-11-18	1	-15/+0
\|\
\| *	Move shared code in new file.	Bernhard Schommer	2020-06-28	1	-16/+0
\| \| \| \| \| \| \| \| \| \|	The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
\| *	Remove the `can_reserve_register` function.	Bernhard Schommer	2020-06-28	1	-2/+0
\| \| \| \| \| \| \| \| \| \|	The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
\| *	Use Hashtbl.find_opt.	Bernhard Schommer	2020-06-28	1	-1/+1
\| \| \| \| \| \| \| \| \| \|	Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* \|	try to be portable across archs	David Monniaux	2019-03-21	1	-2/+7
\|/
*	Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵	Xavier Leroy	2016-10-27	1	-0/+33
	-> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).