aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
...
* | Remove coq warnings (#28)Bernhard Schommer2017-09-229-131/+131
|/
* Constprop strength reduction (#17)Bernhard Schommer2017-07-121-0/+21
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-063-15/+20
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-039-271/+320
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-132-4/+4
* Use "Local" as prefixXavier Leroy2017-02-132-12/+10
* Revised elaboration of attributesXavier Leroy2017-01-312-3/+2
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-18/+0
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+12
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+100
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-019-401/+1004
* Implement support for big endian arm targets.Bernhard Schommer2016-08-051-3/+4
* Unwanted partial constant propagation in 64-bit integer arguments to builtinsXavier Leroy2016-07-081-1/+1
* Port to Coq 8.5pl2Xavier Leroy2016-07-084-33/+32
* common/Determinism.v: dual-license with GPLXavier Leroy2016-06-301-0/+3
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-222-7/+126
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-4/+7
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-172-188/+56
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-0/+916
* Merge branch 'master' into cleanupBernhard Schommer2016-03-218-1966/+2166
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-208-1964/+2164
| |\
| | * Put forward_simulation and backward_simulation in Prop instead of TypeXavier Leroy2016-03-062-303/+323
| | * Add support for EF_runtime externalsXavier Leroy2016-03-062-52/+33
| | * Globalenvs: adapt to new linking framework, and revise.Xavier Leroy2016-03-061-1146/+729
| | * AST: extend and adapt to the new linking framework.Xavier Leroy2016-03-061-460/+116
| | * The basic framework for linking and separate compilation.Xavier Leroy2016-03-061-0/+905
| | * Preliminaries: minor extensions to MemoryXavier Leroy2016-03-061-3/+58
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-2/+2
| |/
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-6/+6
* | Code cleanup.Bernhard Schommer2016-03-103-9/+6
|/
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-4/+8
|\
| * Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-162-0/+2
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1414-1666/+1666
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-143-8/+8
| * Changed the type of the debug sections with additional string.Bernhard Schommer2015-10-132-4/+4
| * Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-132-2/+4
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2017-1673/+1673
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-114-25/+23
|/
* Filled in the rest of the funciton needed for thte debug info under arm.Bernhard Schommer2015-10-092-0/+2
* Added versions of the tranform_* functions in AST to work with functionsBernhard Schommer2015-10-081-1/+216
* Change the way the debug sections are printed.Bernhard Schommer2015-09-282-2/+2
* Added support for the locations of stack allocated local variables.Bernhard Schommer2015-09-252-0/+2
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-223-16/+16
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-213-358/+297
* Represent external worlds by a coinductive type rather than an inductive type.Xavier Leroy2015-06-071-1/+1
* In AST.calling_conventions, record whether the original C function was "old-s...Xavier Leroy2015-05-221-3/+4
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-2/+2
* Typo: Val.sun_inject -> Val.sub_inject.Xavier Leroy2015-05-061-1/+1
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-305-111/+113
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-213-5/+6
generated by cgit (git 2.34.1) at 2024-05-18 05:22:12 +0000