aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-271-1/+2
|\
| * Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-221-1/+2
| | | | | | | | | | | | | | | | | | 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.
* | fix extraction of non-aarch64 targetsSylvain Boulmé2020-12-171-0/+1
| |
* | upgrade kvx backend to coq.8.12.2Sylvain Boulmé2020-12-161-0/+1
| |
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-0/+2
|\|
| * Install "compcert.config" file along the Coq developmentXavier Leroy2020-04-291-0/+1
| | | | | | | | | | | | | | | | The file contains various parameters about the target processor and ABI, useful for VST and possibly other users of CompCert as a Coq library. It is in "var=val" syntax so that it can be included directly from a Makefile or a shell script.
| * Updated .gitignoreBernhard Schommer2020-04-271-0/+1
| | | | | | | | compile.pl is a build artefact.
* | Compiler.v in .gitignoreSylvain Boulmé2020-06-211-0/+1
| |
* | k1c -> kvx changesDavid Monniaux2020-05-261-8/+8
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-081-0/+2
|\| | | | | | | mppa-work-upstream-merge
| * Support Coq 8.11.0 (#212)Xavier Leroy2020-02-051-0/+2
| | | | | | | | Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates.
* | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-161-0/+3
|\| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * AArch64 portXavier Leroy2019-08-081-0/+3
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | More .gitignore for a clean git statusCyril SIX2019-06-191-0/+3
| |
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-1/+4
|\| | | | | | | mppa-if-conversion
| * Ignore more of Coq's cache filesXavier Leroy2019-03-271-1/+4
| | | | | | | | | | A grep through Coq's source files show that it uses more cache files than just .lia.cache. Ignore them all.
* | Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-0/+2
|\| | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h
| * Ignore and clean file .lia.cacheXavier Leroy2019-02-121-1/+3
| | | | | | | | This file is created by Coq when running some tactics
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-211-0/+3
|\| | | | | | | | | Conflicts: .gitignore
| * Ignore generated conflict file. Bug 24455Bernhard Schommer2018-09-101-0/+1
| |
| * Ignore *.v files generated by testsBernhard Schommer2018-06-071-0/+2
| |
* | Fixed MPPA runtimes not compilingCyril SIX2018-11-201-0/+5
| |
* | MPPA - added all shiftsCyril SIX2018-04-171-0/+2
| |
* | MPPA - Running tests in parallelCyril SIX2018-04-101-0/+1
| |
* | MPPA - fixed wrong extension in test filesCyril SIX2018-04-101-0/+2
|/
* Anchor patterns to the top-level directory when appropriateXavier Leroy2018-03-131-47/+47
| | | | | | It's OK to ignore *.o in any directory, but it's safer to ignore "/ccomp" (ccomp in the top-level directory) than to ignore "ccomp" (ccomp in any directory).
* Revert "Update git ignore spec"Bernhard Schommer2017-06-281-1/+0
| | | | This reverts commit 414225093054f0fdd9222e0ba9fbb95d345f5457.
* Update git ignore specMarkus Pister2017-06-281-0/+1
| | | | | | ignore generated directory additional_files Bug 20000
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
* Add a switch to generate a _CoqProject file.Bernhard Schommer2017-02-231-1/+2
|
* Removed CMinor import. Bug 20992Bernhard Schommer2017-02-141-4/+0
|
* Filter macOS metadata files in .gitignoreMichael Schmidt2016-12-281-0/+2
|
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-6/+4
| | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-1/+7
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-201-0/+1
| | | | | | | | 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
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-0/+1
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Ignore .merlin files. Bug 17742Bernhard Schommer2015-12-071-0/+1
|
* Ignore *.cmt(i) files and allow global COMPFLAGS.Bernhard Schommer2015-12-071-0/+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
* Merge remote branch 'upstream/master' into cleanFrançois Pottier2015-10-231-2/+0
|\ | | | | | | | | Conflicts: Makefile.extr
| * We can ignore the generated automation. Bug 17392Bernhard Schommer2015-10-121-0/+1
| |
| * Removal of cchecklink, superseded by AbsInt's Valex tool.Xavier Leroy2015-10-121-2/+0
| |
* | Install the new system for reporting syntax errors.François Pottier2015-10-231-0/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This requires the development version of Menhir, to be released soon. In summary: handcrafted.messages is new. It contains a mapping of erroneous sentences to error messages, together with a lot of comments. Makefile.extr is new. It contains a rule to generate cparser/pre_parser_messages.ml based on this mapping. cparser/ErrorReports.{ml,mli} are new. They construct syntax error messages, based on the compiled mapping. cparser/Lexer.mll is modified. The last two tokens that have been read are stored in a buffer. ErrorReports is called to construct a syntax error message. cparser/GNUmakefile is new. It offers several commands for working on the pre-parser. cparser/deLexer.ml is new. It is a script (it is not linked into CompCert). It translates the symbolic name of a token to an example of this token in concrete C syntax. It is used by [make -C cparser concrete] to produce the .c files in tests/generated/. cparser/tests/generated/Makefile is new. It runs ccomp, clang and gcc on each of the generated C files, so as to allow a comparison of the error messages.
* | A .gitignore entry.François Pottier2015-10-231-0/+1
| |
* | Pass --no-stdlib and -v to menhir when compiling pre_parser.mly.François Pottier2015-10-071-0/+1
|/ | | | | | | Passing --no-stdlib ensures that there is no dependency on Menhir's standard library. Passing -v, which is equivalent to --explain --dump, requests the generation of pre_parser.automaton, a description of the automaton.
* Added Build, Tag, etc in version string and driver/Version.ml should be ignoredBernhard Schommer2015-07-011-1/+1
|
* Added a small ocamlfile that calls ocamlfind recursivly over a given directory.Bernhard Schommer2015-02-241-0/+1
|
* cparser/Parser.v is generated.Xavier Leroy2014-12-301-0/+1
|
* Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵Xavier Leroy2014-11-221-2/+9
| | | | | | produce the executables. configure: add check for GNU make.
* Change the way the tools like the linker, assembler, etc. are specified by ↵Bernhard Schommer2014-09-301-1/+1
| | | | including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
* Add .gitignore files.Xavier Leroy2014-09-211-0/+40
generated by cgit (git 2.34.1) at 2024-05-09 14:02:00 +0000