aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-0/+1
| | | | | | | | | | | | | | 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.
* Removed the version from the compcert.ini file and add it again in a ↵Bernhard Schommer2015-07-011-11/+15
| | | | separate file.
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-5/+4
| | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
* Merge branch 'master' into dwarfBernhard Schommer2015-03-311-0/+2
|\ | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-201-0/+2
| | | | | | | | | | | | | | | | composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.
* | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-0/+1
| | | | | | | | global target dependend option to activate the printing only for targets wher it works.
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-101-3/+3
|\|
| * Removed the glob files from doc/ instead of doc/glob/Bernhard Schommer2015-02-261-1/+1
| |
| * Merge github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-191-1/+1
| |\
| * | Removed the linker flag again.Bernhard Schommer2015-01-201-2/+2
| | |
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-231-1/+1
|\ \ \ | | |/ | |/|
| * | Merge branch 'named-structs'Xavier Leroy2015-01-231-1/+1
| |\ \ | | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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.
| | * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-1/+1
| | | | | | | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-201-4/+4
|\| |
| * | Renamed LIB into VLIB to avoid clashes with environment variables.Bernhard Schommer2015-01-201-2/+2
| | |
| * | Added variable to the Makefile to specify additional linker commands and ↵Bernhard Schommer2015-01-151-2/+2
| | | | | | | | | | | | changed the configure script to deactivated the checklink build if needed.
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-121-48/+25
|\| | | | | | | | | | | | | | Conflicts: powerpc/PrintAsm.ml
| * | No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-181-0/+1
| | | | | | | | | | | | Assorted updates to configure and Makefile.
| * | Merge branch 'master' into pure-makefilesXavier Leroy2014-12-171-10/+12
| |\ \
| * | | Use OCaml's .opt compilers when available.Xavier Leroy2014-12-171-7/+9
| | | | | | | | | | | | | | | | Cleanups in configure.
| * | | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵Xavier Leroy2014-11-221-57/+23
| | | | | | | | | | | | | | | | | | | | | | | | produce the executables. configure: add check for GNU make.
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-171-15/+8
|\ \ \ \ | | |/ / | |/| | | | | | | | | | Conflicts: powerpc/PrintAsm.ml
| * | | Use cp instead of symbolic links for executables.Xavier Leroy2014-12-171-15/+8
| | | | | | | | | | | | | | | | Now that we search for compcert.ini from Sys.executable, symbolic links cause compcert.ini not to be found.
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-111-10/+10
|\| | |
| * | | Preserve single quotes (e.g. in CPREPRO) when generating compcert.iniXavier Leroy2014-12-111-10/+10
| | |/ | |/|
* | | Merge branch 'master' into dwarfBernhard Schommer2014-11-271-0/+1
|\| |
| * | Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-241-0/+1
| |/ | | | | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-271-1/+0
|\|
| * Tune behavior wrt warnings:Xavier Leroy2014-10-241-1/+0
| | | | | | | | | | | | - cchecklink was compiled with -warn-error, which is bad for production code - silence warning 3 (deprecated functions) - silence warning 20 (unused function argument) for Coq-extracted files.
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-201-0/+1
|\|
| * Deactivated the warning for deprecated features for compilation of ↵Bernhard Schommer2014-10-201-0/+1
| | | | | | | | cchecklink since it breaks the build with newer ocaml versions.
* | Added a file containing definitions for the types used to store the debug ↵Bernhard Schommer2014-10-131-1/+1
|/ | | | information. The types follow the Current Attributes by Tag Value in Appendix 1 of the Dwarf 2 standard.
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-091-1/+1
|
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-071-2/+2
|
* Change the way the tools like the linker, assembler, etc. are specified by ↵Bernhard Schommer2014-09-301-21/+23
| | | | including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
* configure: distinguish between ABI and processor model.xleroy2014-07-291-1/+2
| | | | | | | | ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplify COQINCLUDESxleroy2014-07-231-3/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2541 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-231-4/+2
| | | | | | | | | The only platform where we have two variants is ARM, and it's easier to share the callling convention code between the two than to maintain both variants separately. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Redundant -I in CAMLINCLUDESxleroy2014-07-231-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2539 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-231-1/+2
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update Coq documentationv2.3xleroy2014-05-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2483 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-3/+18
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ia32/Select*: complete the modifications to shifts.xleroy2014-04-111-7/+8
| | | | | | | | | Makefile: missing "clean" actions. Makefile/pg/coq: honor $COQBIN if set (as suggested by P. Boutillier) to facilitate testing with different Coq versions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2453 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:xleroy2014-04-061-1/+1
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-1/+1
| | | | | | | the new Lineartyping can't keep track of single floats that were spilled. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Move wt_instr_inv where it belongs.xleroy2014-03-271-1/+1
| | | | | | | Update Makefile and dependencies. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2436 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-1/+1
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-1/+1
| | | | | | | | | | - endianness - alignment constraints for 8-byte types (which is 4 for x86 ABI and 8 for other ABIs) - NaN handling options (superceding the Nan module, removed). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.xleroy2013-12-201-2/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/: new unary operation "addsymbol"xleroy2013-11-171-1/+1
| | | | | | | | Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-28 21:50:24 +0000