aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* 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
|\
| * 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.
* | | Removed the linker flag again.Bernhard Schommer2015-01-201-2/+2
|/ /
* | 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.
* | 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 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.
| * | Preserve single quotes (e.g. in CPREPRO) when generating compcert.iniXavier Leroy2014-12-111-10/+10
| |/
| * 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.
* | 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.
* 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.
* 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.
* 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
* Merge of Flocq version 2.2.0.xleroy2013-08-021-10/+12
| | | | | | | More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-2/+2
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updating LICENSE and license headers, continued.xleroy2013-06-171-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2281 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix compilation of runtime system.xleroy2013-05-291-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2263 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the float32 branch: xleroy2013-05-191-1/+1
| | | | | | | | - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for debugging info (-g).xleroy2013-05-171-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clean up 'make clean'xleroy2013-05-011-2/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2229 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use "-as" to put CompCert modules in a compcert.xxx namespace.xleroy2013-05-011-7/+16
| | | | | | | | Simplified the scripts "coq" and "pg". Updated deps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-11/+8
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated issues with coqchk. See PR#3026 on the Coq bug tracker.xleroy2013-04-141-6/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2189 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted changes to reduce stack and heap requirements when compiling very ↵xleroy2013-03-161-1/+1
| | | | | | big functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-4/+3
| | | | | | | | | | - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More correct exportclight/ dependenciesxleroy2013-01-081-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2094 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Put clighgen files in exportclight/xleroy2013-01-051-7/+10
| | | | | | | | Short doc in exportclight/README git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* RTLgenaux: heuristic to orient if-then-else statements based on sizes.xleroy2012-12-311-2/+4
| | | | | | | Makefile: coqchk notes git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2086 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 16:24:48 +0000