aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.extr
Commit message (Collapse)AuthorAgeFilesLines
* ccomp profilingLéo Gourdin2022-01-051-2/+41
|
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-271-2/+2
|\
| * Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-221-1/+1
| | | | | | | | | | | | | | | | | | As proposed in #404. This is presented as a new option `-clight` to the existing `clightgen` tool. Revise clightgen testing to test the Csyntax output in addition to the Clight output.
| * Refactor clightgenXavier Leroy2021-09-221-2/+2
| | | | | | | | | | | | | | Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-3/+1
|\|
| * Handle the new warnings of OCaml 4.13Xavier Leroy2021-09-131-1/+1
| | | | | | | | | | | | | | | | | | | | | | Warning 69 "mutable record field is never mutated": 3 occurrences in backend/IRC.ml removed the "mutable" qualifier on these fields Warning 70 "cannot find interface file" many .ml files have no .mli no strong motivation to add the .mli files turned off the warning in Makefile.extr
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
| | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-1/+1
|\ \
| * | for OCaml 4.13David Monniaux2021-04-301-1/+1
| | |
* | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-4/+5
|/ / | | | | | | cfrontend/C2C.ml
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-171-3/+26
|\ \
| * \ Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-2/+7
| |\ \ | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * | | Fixing compilation for KVXCyril SIX2020-12-041-1/+1
| | | |
| * | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-3/+26
| |\ \ \ | | | |/ | | |/|
| | * | Do not use -warn-error when building from a release tarballXavier Leroy2020-11-141-2/+9
| | | | | | | | | | | | | | | | | | | | Stopping on warnings is useful for development builds, but unhelpful for released software.
| | * | Bytecode-only build (#243)Xavier Leroy2020-07-071-1/+15
| | | | | | | | | | | | | | | | | | | | | | | | If ocamlopt (the native-code OCaml compiler) is not available, fall back to building with ocamlc (the bytecode OCaml compiler). Fixes: #359
* | | | Merge branch 'kvx-test-prepass' of ↵David Monniaux2020-11-271-2/+6
|\ \ \ \ | |/ / / |/| | / | | |/ | |/| gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass
| * | ccomp.force target for forcing compilation without Coq processingDavid Monniaux2020-10-011-0/+4
| | |
| * | just missing OpWeights for AARCH64David Monniaux2020-09-161-1/+1
| | |
| * | starting to move common filesDavid Monniaux2020-09-161-1/+1
| | |
| * | Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-281-2/+2
| |\ \ | |/ / |/| | | | | | | | Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand framework
| * | Adding stub RTLpathLivegenaux.mlCyril SIX2020-05-251-1/+2
| | |
* | | k1c -> kvx changesDavid Monniaux2020-05-261-1/+1
|/ /
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-081-4/+3
|\| | | | | | | mppa-work-upstream-merge
| * Compatibility with OCaml 4.10 (#214)Xavier Leroy2020-02-061-2/+2
| | | | | | | | | | | | | | | | debug/DwarfPrinter.mli: unused functor parameter trigger warning 69, replace by non-dependent functor type. Makefile.extr: turn warning 69 (unused functor parameter) off for extracted code configure: accept OCaml versions above 4.09 configure: update messages for unsupported versions of OCaml and Coq
| * Revised menhirLib autoconfiguration (#331)Xavier Leroy2020-02-051-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since Menhir version 20200123, we need to link with menhirLib.cmxa instead of menhirLib.cmx. This commit chooses automatically the file to link with: menhirLib.cmxa if it exists in the menhirLib installation directory, menhirLib.cmx otherwise. To reliably find the installation directory, configure was changed to record the menhirLib directory in Makefile.config, variable MENHIR_DIR, instead of a pre-cooked command-line option MENHIR_INCLUDES. Makefile.extr was adapted accordingly. Fixes: #329 Closes: #330
* | various fixesDavid Monniaux2019-07-191-1/+1
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-3/+4
|\| | | | | | | mppa-work-upstream-merge
| * New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | What's new: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree. The corresponding changes in Menhir have been released as part of version 20190626. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed.
* | compilation of ImpIOOraclesSylvain Boulmé2019-03-051-1/+1
| |
* | Adding Mem as a possible location for accessesCyril SIX2019-01-111-1/+1
| |
* | quick and dirty Makefile fixesSylvain Boulmé2019-01-111-2/+2
| |
* | Removed warning 42 from OCamlCyril SIX2019-01-081-1/+1
|/ | | | CompCert does not support OCaml version <= 4.00
* Removed CMinor import. Bug 20992Bernhard Schommer2017-02-141-7/+3
|
* Add LINK_OPT and document it.Bernhard Schommer2017-02-011-2/+15
| | | | | | | The new Makefile variable LINK_OPT can be used to specify additional linker flags for different operating systems, like linking with setargv.obj under windows. Bug 20871
* Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-201-1/+2
| | | | | | | | The functions expandargv and writeargv resemble the functions from the libiberity that are used by the gnu tools. Additionaly a new configuration is added in order to determine which kind of response files are supported for calls to other tools. Bug 18308
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-211-3/+1
| | | | | | | | Most of the code can be String.uppercase usages can either be replaced by a more specialized version of coqstring_of_camlstring (which is also slightly more effecient) or by specialized checks that reject wrong code earlier. Bug 19187
* Moved shared frontend code in own file.Bernhard Schommer2016-05-241-1/+1
| | | | | | | Clightgen and CompCert share the code for preprocessing as well as parsing C files. The code as well as command line switches is moved in the new module Frontend. Bug 18768
* Split dependency generation.Bernhard Schommer2016-05-131-1/+2
| | | | | | GNU make under windows seems to have a restriction to 8192 characters for commandline arguments. The dependency generation of compcert is too large. Thus we split it into two steps.
* Compatibility with newer ocaml versions. Bug 18313.Bernhard Schommer2016-03-311-1/+5
|
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-1/+1
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-101-3/+3
| | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
* Added warning for strict-sequences.Bernhard Schommer2016-01-211-1/+1
|
* Removed the last remains of cchecklink.Bernhard Schommer2016-01-211-2/+0
|
* Ignore *.cmt(i) files and allow global COMPFLAGS.Bernhard Schommer2015-12-071-4/+2
| | | | | | | Instead of using = to set the COMPFLAGS use += which allows it to specify custom compiler flags in for example the Makefile.config. Also remove *.cmt(i) files and add them to the .gitignore file. Bug 17742
* Tentative fix for issue #70 (menhirLib recompilation problems)Xavier Leroy2015-11-131-2/+2
| | | | Don't pass $(MENHIR_INCLUDES) to ocamldep.
* Merge remote branch 'upstream/master' into cleanFrançois Pottier2015-10-231-53/+3
|\ | | | | | | | | Conflicts: Makefile.extr
| * Merge branch 'clean' of https://github.com/fpottier/CompCert into fpottier-cleanBernhard Schommer2015-10-201-6/+9
| |\ | | | | | | | | | | | | Conflicts: Makefile.extr
| * | Removal of cchecklink, superseded by AbsInt's Valex tool.Xavier Leroy2015-10-121-53/+3
| | |
* | | Added a few cleanup commands in [make clean].François Pottier2015-10-231-1/+2
| | |
generated by cgit (git 2.34.1) at 2024-05-09 19:27:57 +0000