aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Introduce 'cmn' instruction and optimize compare-with-immediate when negated ...Michael Schmidt2017-12-156-1/+27
* Moved constant expansion into Asmexpand. (#40)Bernhard Schommer2017-12-145-318/+419
* Use instructions with immediate operands that don't need replacement by the a...Michael Schmidt2017-12-141-4/+3
* Export configured architecture to JSON (#38)Michael Schmidt2017-12-132-3/+9
* Do not pass the env back from for stmt decls. (#42)Bernhard Schommer2017-12-121-7/+7
* Deactivate ais_annotations again.Bernhard Schommer2017-12-121-24/+25
* Merge pull request #210 from ppedrot/fix-coq-6277Xavier Leroy2017-12-111-1/+1
|\
| * Fix check-proof target of the Makefile after merge of Coq #6277.Pierre-Marie Pédrot2017-12-071-1/+1
* | Correct test for noinline. Bug 22642Bernhard Schommer2017-12-111-1/+1
* | Test for inline. Bug 22642Bernhard Schommer2017-12-081-1/+1
* | Introduce and use C2C.atom_inline function with 3-valued resultXavier Leroy2017-12-082-14/+11
* | Remove unused code. BUg 22642Bernhard Schommer2017-12-082-3/+2
* | Store the different inlining cases.Bernhard Schommer2017-12-083-10/+28
* | Do not inline varag functions. Bug 22642Bernhard Schommer2017-12-071-3/+3
|/
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-077-13/+105
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-058-36/+85
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-012-0/+40
* Remove unused float_abi_type.Bernhard Schommer2017-11-291-12/+0
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-11-270-0/+0
|\
| * Remove temporary .o files after linking (#36)Xavier Leroy2017-11-271-2/+5
* | Remove temporary .o files after linking (#36)Xavier Leroy2017-11-271-2/+5
|/
* Issue #208: make value analysis of comparisons more conservative w.r.t. point...Xavier Leroy2017-11-242-8/+15
* Pull request #192: improve the printing of Clight intermediate codeXavier Leroy2017-11-223-10/+29
* Added json export for the abstract ARM AssemblerBernhard Schommer2017-11-202-64/+338
* Moved arm eabi fixup to Asmexpand.Bernhard Schommer2017-11-163-159/+229
* New json printing interface.Bernhard Schommer2017-11-144-144/+208
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-105-8/+0
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-095-105/+1
* 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-084-5/+8
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-084-92/+71
* Remove superfluous function.Bernhard Schommer2017-11-066-11/+2
* Also quote \a.Bernhard Schommer2017-10-261-0/+2
* Fix register name of ais printing and moved label function up.Bernhard Schommer2017-10-251-4/+4
* Remove ais_annot_intval.Bernhard Schommer2017-10-241-13/+0
* Prefix ais annotations with location.Bernhard Schommer2017-10-241-2/+4
* Coq 8.7.0 supportXavier Leroy2017-10-202-3/+8
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-2015-3/+15
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-2015-3/+15
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-1931-66/+180
* | Check recursively for const for modifiable lvalues (#32)Bernhard Schommer2017-10-171-2/+15
* | Do not generate object files for linking.Bernhard Schommer2017-10-161-7/+14
* | Distinguish between long and int for cases.Bernhard Schommer2017-10-131-7/+7
* | Make the list unique. Bug 22239Bernhard Schommer2017-09-261-177/+22
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-265-34/+11
* | Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-09-250-0/+0
|\ \
| * | Remove coq warnings (#28)Bernhard Schommer2017-09-2272-638/+638
* | | Added dump-mnemonics option.Bernhard Schommer2017-09-258-2/+208
* | | Remove coq warnings (#28)Bernhard Schommer2017-09-2272-638/+638
|/ /
generated by cgit (git 2.34.1) at 2024-07-01 05:39:00 +0000