aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-102-2/+0
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-091-1/+0
* Use address for printing address constant. Bug 22525Bernhard Schommer2017-11-091-2/+3
* Generalize print_init.Bernhard Schommer2017-11-091-1/+40
* Fix jumptable issue.Bernhard Schommer2017-11-081-2/+5
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-081-6/+21
* Remove superfluous function.Bernhard Schommer2017-11-062-3/+2
* Also quote \a.Bernhard Schommer2017-10-261-0/+2
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-205-0/+5
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-205-0/+5
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-197-9/+37
* | Distinguish between long and int for cases.Bernhard Schommer2017-10-131-7/+7
* | Remove coq warnings (#28)Bernhard Schommer2017-09-2225-179/+179
* | Deadcode: eliminate trivial Icond instructionsXavier Leroy2017-09-182-2/+9
* | Prefixed runtime functions.Bernhard Schommer2017-08-252-45/+45
* | Asmgenproof0: some more useful lemmasXavier Leroy2017-08-171-0/+29
* | Print_annot should produce a string.Bernhard Schommer2017-07-191-26/+25
|/
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-0/+2
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-0618-10/+95
* Inliningspec made compatible with a coming fix of zifyletouzey2017-05-271-1/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-0327-342/+711
* Tunnelingproof: Remove assumption destroyed_by_cond c = nil.Xavier Leroy2017-05-021-66/+210
* RISC-V port and assorted changesXavier Leroy2017-04-284-43/+117
* Modest optimization of leaf functionsXavier Leroy2017-04-281-2/+75
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-071-1/+3
* Add optimization option finline.Bernhard Schommer2017-04-071-1/+1
* Another optimization of empty if/else and other useless conditional branchesXavier Leroy2017-04-062-31/+41
* use 'f' as generic function-identifier instead of arbitraty identifier 1 for ...Michael Schmidt2017-03-231-1/+1
* Removed CMinor import. Bug 20992Bernhard Schommer2017-02-145-1298/+0
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-3/+5
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-131-2/+2
* Use "Local" as prefixXavier Leroy2017-02-135-6/+6
* Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maxime...Xavier Leroy2017-02-134-6/+7
|\
| * Fix broken fragile automation.Maxime Dénès2017-01-091-1/+2
| * Subst's behavior on let-ins has changed.Maxime Dénès2017-01-091-2/+2
| * The subst tactic has become more powerful.Maxime Dénès2017-01-092-3/+3
* | Inlined open of ErrorsBernhard Schommer2017-02-061-10/+9
* | Datatypes no longer shadows fst and sndBernhard Schommer2017-02-061-1/+1
* | Remove open Locations.Bernhard Schommer2017-02-061-6/+5
* | Remove open Locations.Bernhard Schommer2017-02-061-6/+5
* | Remove unused openBernhard Schommer2017-02-061-1/+0
|/
* Use 64 bit address in debug information.Bernhard Schommer2016-11-102-0/+2
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-6/+6
* SplitLong: propagate constants through "longofint"Xavier Leroy2016-10-252-4/+8
* Update ARM port. Not tested yet.Xavier Leroy2016-10-253-7/+8
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-046-17/+337
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+1
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-027-132/+256
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-0138-1197/+1624
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-211-4/+4
|\
generated by cgit (git 2.34.1) at 2024-06-02 21:14:11 +0000