aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* try to get it to compileDavid Monniaux2020-03-031-0/+1
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-141-1/+1
|\
| * Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-081-1/+1
| |\
| | * Support Coq 8.11.0 (#212)Xavier Leroy2020-02-051-1/+1
* | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-0/+1
|\ \ \ | |/ / |/| |
| * | CSE2 split in two filesDavid Monniaux2020-01-281-0/+1
| |/
* | connect forward-moves to compilerDavid Monniaux2020-01-081-0/+1
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-0/+1
|\ \
| * | Stubs for Duplicate passCyril SIX2019-09-031-0/+1
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-non-tra...David Monniaux2019-09-101-0/+1
|\ \ \ | |/ / |/| / | |/
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-281-0/+1
|\|
| * Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-051-0/+1
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-12/+12
|\|
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-1/+1
| * New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-11/+11
| * Type inference and type checking for CminorXavier Leroy2019-06-061-1/+1
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-031-25/+22
|\ \
| * | Type inference and type checking for CminorXavier Leroy2019-05-311-1/+1
| |/
| * Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-171-12/+12
| * Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-261-1/+1
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+1
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-11/+8
* | ça recompile sur x86David Monniaux2019-03-221-1/+1
* | Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-5/+2
|\|
| * Ignore and clean file .lia.cacheXavier Leroy2019-02-121-0/+1
| * Make the checker happy (#272)Vincent Laporte2019-02-121-5/+1
* | 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
generated by cgit (git 2.34.1) at 2024-06-02 19:13:04 +0000