aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
...
* | Adding Mem as a possible location for accessesCyril SIX2019-01-111-0/+1
* | compilation Asmexpandaux both for x86/ and mppa_k1c/Sylvain Boulmé2018-11-281-1/+1
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-4/+5
* | Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-261-3/+3
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-211-13/+20
|\|
| * Make generated file cparser/Parser.v read-onlyXavier Leroy2018-08-271-0/+2
| * Ensure compatibility with Menhir before and after version 20180530Xavier Leroy2018-06-061-1/+1
| * Fix menhirLib namespaces, following changes in Menhir version 20180530Jacques-Henri Jourdan2018-06-061-2/+2
| * Use the standalone coq2html tool to generate the HTML documentationXavier Leroy2018-06-011-10/+2
| * Install the VERSION file along the .vo filesBenoît Viguier2018-05-311-0/+1
| * Install Coq development (.vo files) if requested (#232)Xavier Leroy2018-05-301-1/+10
| * Upgrade Flocq to version 2.6.1 from upstream (#71)Xavier Leroy2018-04-251-0/+3
* | Removed the bundle attemptCyril SIX2018-09-281-1/+0
* | MB2AB - un peu d'avancement sur internal functionCyril SIX2018-09-251-1/+1
* | a few stubs for bundlingSylvain Boulmé2018-09-241-0/+1
* | premier jet Asmblockgenproof.return_address_offsetSylvain Boulmé2018-09-181-1/+1
* | Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-061-1/+1
* | Asmblock: Adding forward_simulation and determinism as axiomsCyril SIX2018-09-061-1/+1
* | Asmblockgen.v finished (no proof yet)Cyril SIX2018-09-061-1/+1
* | Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléterCyril SIX2018-09-061-0/+1
* | Machblock: Mach language with basic blocksCyril SIX2018-09-061-1/+2
|/
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-281-3/+0
* Removed no longer needed struct passing.Bernhard Schommer2018-02-261-2/+0
* Fix check-proof target of the Makefile after merge of Coq #6277.Pierre-Marie Pédrot2017-12-071-1/+1
* Makefile: chmod a-w instead of chmod -wXavier Leroy2017-09-111-1/+1
* Update the "make check-proof" entry for Coq 8.6Xavier Leroy2017-03-241-3/+2
* Turn warning "deprecated-implicit-arguments" off while compiling FlocqXavier Leroy2017-02-131-1/+4
* Also remove coq aux files.Bernhard Schommer2017-01-241-0/+1
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-1/+1
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-271-10/+26
|\
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-8/+23
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-2/+3
* | Add a man-pageMichael Schmidt2016-10-141-0/+2
|/
* fix merge conflictsMichael Schmidt2016-08-171-1/+2
|\
| * Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-201-1/+2
* | Implement support for big endian arm targets.Bernhard Schommer2016-08-051-0/+1
|/
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-8/+5
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-281-1/+0
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-2/+3
* Also enable warnings for doc generator.Bernhard Schommer2016-04-061-2/+2
* Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-1/+2
* Split up tools and options.Bernhard Schommer2016-02-251-1/+4
* Added configuration to enable clightgen build.Bernhard Schommer2015-12-281-10/+6
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-0/+1
* Removed the version from the compcert.ini file and add it again in a separate...Bernhard Schommer2015-07-011-11/+15
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-5/+4
* Merge branch 'master' into dwarfBernhard Schommer2015-03-311-0/+2
|\
| * Improvements in the StructReturn transformation (ABI conformance for passing ...Xavier Leroy2015-03-201-0/+2
* | Started implementing the printing functions for the debug info. Added a globa...Bernhard Schommer2015-03-161-0/+1
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-101-3/+3
|\|
generated by cgit (git 2.34.1) at 2024-05-20 06:35:09 +0000