compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
...
\| \| * \| \|	Merge branch 'no-shell' of github.com:AbsInt/CompCert into compcert_windows	Bernhard Schommer	2015-02-19	5	-96/+272
\| \| \|\ \ \
\| \| \| * \ \	Merge branch 'master' into no-shell	Bernhard Schommer	2015-02-19	81	-2496/+6257
\| \| \| \|\ \ \ \| \| \|_\|/ / / \| \|/\| \| \| \|
\| \| \| * \| \|	Use Unix.create_process instead of Sys.command (continued).	Xavier Leroy	2014-12-29	3	-96/+122
\| \| \| \| \| \|
\| \| \| * \| \|	Use Unix.create_process instead of Sys.command to run external tools.	Xavier Leroy	2014-12-19	2	-0/+150
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Revised parsing of compcert.ini file to split arguments into words like POSIX shell does (including quotes).
\| \| * \| \| \|	Merge github.com:AbsInt/CompCert into compcert_windows	Bernhard Schommer	2015-02-19	66	-2277/+5719
\| \| \|\ \ \ \ \| \| \|/ / / / \| \|/\| \| \| \|
\| * \| \| \| \|	The parameter should also have the old name.	Bernhard Schommer	2015-02-19	1	-3/+3
\| \| \| \| \| \|
\| \| * \| \| \|	Removed the linker flag again.	Bernhard Schommer	2015-01-20	2	-4/+4
\| \| \| \| \| \|
* \| \| \| \| \|	Removed the MinGW port.	Bernhard Schommer	2015-02-19	1	-53/+3
\| \| \| \| \| \|
* \| \| \| \| \|	Merge github.com:AbsInt/CompCert	Bernhard Schommer	2015-02-19	19	-15/+935
\|\\| \| \| \| \|
* \| \| \| \| \|	Use lcomm instead of .local for Mingw.	Bernhard Schommer	2015-02-10	1	-2/+2
\| \| \| \| \| \|
* \| \| \| \| \|	Added new Mingw Printer. Currently the only difference to the Cygwin printer ↵	Bernhard Schommer	2015-02-10	1	-13/+55
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	is that every symbol must start with an "_".
\| \| \| \| * \|	Merge branch 'master' into backend_printer	Bernhard Schommer	2015-02-19	18	-8/+928
\| \| \| \| \|\ \ \| \| \|_\|_\|/ / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: ia32/PrintAsm.ml
\| * \| \| \| \|	Added back symbol functions in the different printer, since they are still ↵	Bernhard Schommer	2015-02-19	1	-3/+10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	needed.
\| * \| \| \| \|	Changed the symbol function back to its old definition.	Bernhard Schommer	2015-02-19	1	-10/+3
\| \| \| \| \| \|
\| * \| \| \| \|	C reference implementation of the int64 helper functions.	Xavier Leroy	2015-02-14	18	-8/+928
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In test_int64.c: don't test FP->int64 conversions when the FP argument is out of range.
\| \| \| * \|	Removed unused sel_target, changed cygwin symbol names and changed the ↵	Bernhard Schommer	2015-02-19	5	-7/+11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	default function aligment to be target dependent.
\| \| \| * \|	Added an elf prefix to all common elf functions in PrintAsmaux.	Bernhard Schommer	2015-02-18	5	-36/+50
\| \| \| \| \|
\| \| \| * \|	Changed print_fun/var_info to be functions instead of booleans.	Bernhard Schommer	2015-02-18	5	-18/+16
\| \| \| \| \|
\| \| \| * \|	Removed some style issues.	Bernhard Schommer	2015-02-18	3	-76/+82
\| \| \| \| \|
\| \| \| * \|	Changed arm backend to the common backend printer.	Bernhard Schommer	2015-02-09	7	-1194/+1145
\| \| \| \| \|
\| \| \| * \|	Merge remote-tracking branch 'origin/master' into backend_printer	Bernhard Schommer	2015-02-09	3	-231/+226
\| \| \| \|\ \ \| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	Interpreter produces more detailed trace, including name of semantic rules used.	Xavier Leroy	2015-02-08	3	-231/+226
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Cexec: record names of rules used in every reduction. Interp: print these rule names in -trace mode. Also: simplified the exploration in "-all" mode; give unique names to states. Csem: fix name of reduction rule "red_call".
\| \| \| * \|	Changed the ia32 backend to the new Printer.	Bernhard Schommer	2015-02-06	5	-1035/+983
\| \| \| \| \|
\| \| \| * \|	Changed the ASM printer of the powerpc to the generalized backend.	Bernhard Schommer	2015-02-05	5	-792/+850
\| \| \| \| \|
\| \| \| * \|	Moved more common functions into a seperate file.	Bernhard Schommer	2015-02-04	4	-137/+69
\| \| \| \| \|
\| \| \| * \|	Started moving common backend functions into one file.	Bernhard Schommer	2015-02-03	3	-84/+114
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Changed the print_globaldef function of the powerpc backend to look like the ↵	Bernhard Schommer	2015-01-28	1	-10/+2
\| \|_\|/ \|/\| \| \| \| \| \| \| \|	functions used in the arm and ia32 backend.
* \| \|	Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.	Xavier Leroy	2015-01-23	1	-70/+122
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of assuming name uniqueness for all definitions in the program, these variants only assume uniqueness for a particular name. Use this approach to weaken the hypotheses for match_program and transf_program_partial_augment.
* \| \|	Merge branch 'named-structs'	Xavier Leroy	2015-01-23	36	-1630/+4023
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
\| * \| \|	Define a nonnegative integer "rank" for types to support structural ↵	Xavier Leroy	2015-01-10	2	-22/+120
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	induction over composite types.
\| * \| \|	Add a type system for CompCert C and type-checking constructor functions.	Xavier Leroy	2014-12-31	8	-80/+2101
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
\| * \| \|	Represent struct and union types by name instead of by structure.	Xavier Leroy	2014-12-22	23	-1320/+1535
\| \| \| \|
\| * \| \|	Make small-step semantics more parametric w.r.t. the type of global ↵	Xavier Leroy	2014-11-26	2	-27/+42
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	environments. Use symbol environments for the part of semantics that deals with observable events.
\| * \| \|	Introduce symbol environments (type Senv.t) as a restricted view on global ↵	Xavier Leroy	2014-11-26	9	-201/+245
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
* \| \| \|	Delay reads from !Machine.config before it is properly initialized.	Xavier Leroy	2015-01-22	8	-68/+88
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Several definitions in Cutil and elsewhere were accessing the default value of !Machine.config, before it is properly initialized in Driver. Delay evaluation of these definitions, and initialize Machine.config to nonsensical values so that lack of initialization is caught early (e.g. in Cutil.find_matching_*_kind). Also, following up on commit [3b8a094], don't use "wchar_t" typedef to type wide string literals, even if this typedef is in scope. The risk here is to hide an inconsistency between "wchar_t"'s definition in standard headers and CompCert's built-in definition.
* \| \| \|	Merge branch containing changes for windows compile.	Bernhard Schommer	2015-01-20	3	-8/+15
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Renamed LIB into VLIB to avoid clashes with environment variables.	Bernhard Schommer	2015-01-20	1	-2/+2
\| \| \| \|
\| * \| \|	Replaced 8 spaces by tabs.	Bernhard Schommer	2015-01-16	1	-1/+1
\| \| \| \|
\| * \| \|	Added new target to just remove the cm[iox] files and the build executables.	Bernhard Schommer	2015-01-16	1	-0/+4
\| \| \| \|
\| * \| \|	Added missing $ for build_checklink	Bernhard Schommer	2015-01-15	1	-2/+2
\| \| \| \|
\| * \| \|	Added variable to the Makefile to specify additional linker commands and ↵	Bernhard Schommer	2015-01-15	3	-6/+9
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	changed the configure script to deactivated the checklink build if needed.
* \| \| \|	Protect against redefinition of the __i64_xxx helper library functions.	Xavier Leroy	2015-01-20	6	-251/+306
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions.
* \| \| \|	Follow-up to [5aecefe]: be conservative also in the case of a "common" ↵	Xavier Leroy	2015-01-20	1	-6/+21
\|/ / / \| \| \| \| \| \| \| \| \|	global const variable.
* \| \|	More prudent analysis of uninitialized const global variables.	Xavier Leroy	2015-01-09	1	-3/+6
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In the presence of separate compilation and linking, an uninitialized const global variable may be initialized elsewhere with a pointer value, falsifying the points-to analysis. Report and fix by Chung-Kil Hur and Jeehoon Kang.
* \| \|	In -g -S mode, annotate the generated asm file with the C source code in ↵	Xavier Leroy	2015-01-07	6	-86/+243
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml
* \| \|	PR#19: there is no reason to reject an empty "switch" statement.	Xavier Leroy	2015-01-06	1	-2/+0
\| \| \|
* \| \|	PR#16: give option rules precedence over file pattern rules.	Xavier Leroy	2015-01-03	3	-31/+38
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Plus: simplify handling of -help and --help. Plus: error on unrecognized "-xxx" options so that "-foo.c" is not treated as a source file.
* \| \|	PR#14: recognize ".so" arguments as files to pass to the linker.	Xavier Leroy	2015-01-02	1	-1/+2
\| \| \|
* \| \|	PR#15: vararg functions are not eligible for inlining.	Xavier Leroy	2015-01-02	1	-1/+1
\| \| \|
* \| \|	Translation of wide string literals.	Xavier Leroy	2015-01-01	1	-6/+57
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Closes PR#13. Also: give string literals type unsigned char [] or signed char [] depending on the machine configuration. (Instead of unsigned char [] before.)