compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Fixed minor typos in the comments.	Bernhard Schommer	2015-10-04	1	-1/+1
\|
*	Add the forgotten Fileinfo also to arm and ia32 TargetPrinter.ml	Bernhard Schommer	2015-10-02	1	-0/+1
\|
*	Cleanup of now no longer needed functions.	Bernhard Schommer	2015-10-01	1	-11/+1
\|
*	Change the way the debug sections are printed.	Bernhard Schommer	2015-09-28	1	-1/+1
\| \| \| \| \| \|	If a user uses the #pragma use_section for functions the diab linker requires a separate debug_info section for each entry. This commit adds functionality to emulate this behavior.
*	Added printing the reference address for the LocRef and started refactoring old	Bernhard Schommer	2015-09-27	1	-9/+1
\| \| \| \| \| \| \| \|	Debuging code. The old functions to store the symbol for the Global variables and retrive this is no longer needed since the atom is stored in DebugInformation. Also the Debug.Abbrev module is no longer needed.
*	Added support for the locations of stack allocated local variables.	Bernhard Schommer	2015-09-25	1	-0/+1
\| \| \| \| \|	This commit adds furher support for location information for local variables and starts with the implementation of the debug_loc section.
*	Record the scope structure during unblocking.	Bernhard Schommer	2015-09-22	1	-0/+2
\| \| \| \| \| \|	Instead of creating separate annotations for the local variables we call the Debug.add_lvar_scope and we construct a mapping from function id + scope id to scope information.
*	Revert "Startet implementation of new Debug interface."	Bernhard Schommer	2015-09-10	1	-1/+0
\| \| \| \|	This reverts commit 861292a6c5e58b4f78bef207c717b801b3fc1fed.
*	Startet implementation of new Debug interface.	Bernhard Schommer	2015-09-06	1	-0/+1
\| \| \| \| \| \|	Added a new file debug/Debug.ml which will be the interface between for generating and printing the debuging information. Currently it contains only the code for the line directived.
*	X	Bernhard Schommer	2015-09-06	8	-209/+256
\|\ \| \| \| \| \| \|	Merge branch 'master' into debug_locations
\| *	Upgrade the ARM port to the new builtins.	Xavier Leroy	2015-08-24	8	-209/+256
\| \|
* \|	Merge branch 'master' into debug_locations	Bernhard Schommer	2015-08-26	1	-11/+12
\|\\| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: debug/CtoDwarf.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli
\| *	Asmexpand for ARM: fixed bug in Pfreeframe.	Xavier Leroy	2015-08-21	1	-3/+3
\| \| \| \| \| \| \| \|	Plus: update comments and credit Bernhard Schommer.
\| *	Fix bugs in Asmexpand.ml for ARM.	Xavier Leroy	2015-08-21	1	-8/+9
\| \|
* \|	Added symbol functions for printing of the location for global variables.	Bernhard Schommer	2015-08-21	1	-0/+6
\|/
*	Merge pull request #46 from AbsInt/asmexpand	Xavier Leroy	2015-08-17	3	-283/+443
\|\ \| \| \| \|	Merge branch 'asmexpand' of github.com:AbsInt/CompCert
\| *	Updated the branch and implemented the suggested changes.	Bernhard Schommer	2015-07-14	3	-44/+78
\| \|
\| *	Merge branch 'master' into asmexpand	Bernhard Schommer	2015-07-14	1	-0/+18
\| \|\
\| * \|	Merge branch 'asmexpand' of github.com:AbsInt/CompCert	Bernhard Schommer	2015-06-26	3	-283/+409
\| \| \|
\| * \|	Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"	Bernhard Schommer	2015-06-26	3	-409/+283
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
\| * \|	Moved the rest of the ia32 builtins to asmexpand.	Bernhard Schommer	2015-06-22	1	-1/+3
\| \| \|
\| * \|	Moved the printing of the builtin functions etc. into Asmexpand for ARM in ↵	Bernhard Schommer	2015-06-10	3	-283/+407
\| \| \| \| \| \| \| \| \| \| \| \|	the same way as it is done for PPC.
* \| \|	Value analysis: keep track of pointer values that leak through small ↵	Xavier Leroy	2015-07-19	2	-21/+21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	integers with Uns or Sgn abstract values. This is a follow-up to commit 2932b53. It adds provenance tracking to the Uns and Sgn abstract values.
* \| \|	Value analysis: keep track of pointer values that leak through arithmetic ↵	Xavier Leroy	2015-07-19	1	-2/+2
\| \|/ \|/\| \| \| \| \| \| \| \| \|	operations with undefined behaviors. Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value. "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer). In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.
* \|	Merge branch 'master' into json_export	Bernhard Schommer	2015-05-18	5	-31/+68
\|\\|
\| *	Merged PrintAnnot into PrintAsmaux.	Bernhard Schommer	2015-05-14	1	-4/+4
\| \|
\| *	Updated PrintOp for the single-precision FP operations.	Xavier Leroy	2015-05-09	1	-0/+21
\| \|
\| *	Extended inline asm: revised treatment of clobbered registers.	Xavier Leroy	2015-05-09	3	-27/+43
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* \|	Merge branch 'master' into json_export	Bernhard Schommer	2015-05-07	1	-4/+4
\|\\|
\| *	Typo: Val.sun_inject -> Val.sub_inject.	Xavier Leroy	2015-05-06	1	-4/+4
\| \|
* \|	Merge branch 'master' into json_export	Bernhard Schommer	2015-05-05	1	-47/+47
\|\\|
\| *	Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵	Xavier Leroy	2015-04-30	1	-47/+47
\| \| \| \| \| \| \| \|	Val.lessdef, etc.
* \|	Added the first version of the sdump export to json.	Bernhard Schommer	2015-04-27	1	-0/+18
\|/
*	Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵	Xavier Leroy	2015-04-23	2	-1/+4
\| \| \| \|	clobber lists.
*	Take asm clobbers into account for determining callee-save registers used.	Xavier Leroy	2015-04-23	2	-0/+8
\|
*	Cleanups and updates for extended asm.	Xavier Leroy	2015-04-21	1	-1/+1
\|
*	Support for GCC-style extended asm, continued:	Xavier Leroy	2015-04-21	1	-1/+1
\| \| \| \| \| \| \| \|	- support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
*	Experiment: support a subset of GCC's extended asm statements.	Xavier Leroy	2015-04-17	2	-2/+6
\|
*	Correct type of label function.	Bernhard Schommer	2015-04-16	1	-1/+1
\|
*	Added missing dummy functions.	Bernhard Schommer	2015-04-16	1	-0/+4
\|
*	Merge branch 'master' into dwarf	Bernhard Schommer	2015-04-04	2	-3/+5
\|\
\| *	Fixed missing unsigned compare for pointer in the arm backend.	Bernhard Schommer	2015-04-04	2	-3/+5
\| \|
* \|	Merge branch 'master' into dwarf	Bernhard Schommer	2015-04-02	5	-46/+41
\|\\|
\| *	Updating the PowerPC and ARM ports.	Xavier Leroy	2015-03-27	5	-46/+41
\| \| \| \| \| \| \| \|	PowerPC: always use full register names to print annotations.
* \|	Merge branch 'master' into dwarf	Bernhard Schommer	2015-03-23	1	-2/+6
\|\\|
\| *	Fix .type and .size annotations: @ is comment, use % instead.	Xavier Leroy	2015-03-20	1	-2/+6
\| \|
* \|	Merge branch 'master' into dwarf	Bernhard Schommer	2015-03-16	1	-0/+1
\|\\|
\| *	Missing initialization of current_function_sig.	Xavier Leroy	2015-03-14	1	-0/+1
\| \|
* \|	Started implementing the printing functions for the debug info. Added a ↵	Bernhard Schommer	2015-03-16	1	-0/+6
\| \| \| \| \| \| \| \|	global target dependend option to activate the printing only for targets wher it works.
* \|	Started integrating the debug printing in the common backend_printer.	Bernhard Schommer	2015-03-11	1	-0/+6
\|/