aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* 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
|\
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-211-4/+4
* | Add interference for indirect calls.Bernhard Schommer2016-09-151-1/+4
* | Removed some implict arguments.Bernhard Schommer2016-09-051-15/+6
* | Merge pull request #118 from AbsInt/armebXavier Leroy2016-08-241-4/+7
|\ \
| * | Implement support for big endian arm targets.Bernhard Schommer2016-08-051-4/+7
| |/
* / PR#113, PR#122: Unspillable temporaries causing register allocation to failXavier Leroy2016-08-241-1/+6
|/
* Merge pull request #105 from m-schmidt/masterXavier Leroy2016-07-112-0/+5
|\
| * add 'runtime' token to lexerMichael Schmidt2016-07-011-0/+1
| * extend cminor parser to accept "extern runtime" declarationsMichael Schmidt2016-07-011-0/+4
* | Port to Coq 8.5pl2Xavier Leroy2016-07-086-39/+36
|/
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-281-3/+3
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-223-2/+28
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-222-35/+63
generated by cgit (git 2.34.1) at 2024-06-02 16:01:26 +0000