aboutsummaryrefslogtreecommitdiffstats
path: root/x86
Commit message (Expand)AuthorAgeFilesLines
...
* | try to be portable across archsDavid Monniaux2019-03-213-3/+11
|/
* x86: wrong modeling of ZF flag for FP comparisonsXavier Leroy2018-12-202-130/+66
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-123-6/+7
* Fix expansion of ctzl/clzl builtin for 64bit targets (#127)Michael Schmidt2018-07-121-2/+15
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-012-3/+12
* Fix register naming for stack pointer.Bernhard Schommer2018-03-081-3/+4
* Removed % prefix from ais annot register names.Bernhard Schommer2018-03-081-1/+18
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-061-5/+5
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-162-15/+49
* Switching the cases seems to work on x86_32Bernhard Schommer2018-02-121-2/+2
* In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bitsXavier Leroy2018-02-123-11/+33
* x86 ConstpropOp.addr_strength_reduction: always check validity of resulting a...Xavier Leroy2018-02-082-10/+15
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-4/+12
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-052-10/+24
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-101-2/+0
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-091-28/+0
* Fix jumptable issue.Bernhard Schommer2017-11-081-1/+1
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-081-15/+11
* Remove superfluous function.Bernhard Schommer2017-11-061-2/+0
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-0/+1
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-0/+1
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-193-8/+18
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-261-8/+0
* | Added dump-mnemonics option.Bernhard Schommer2017-09-252-0/+4
* | Remove coq warnings (#28)Bernhard Schommer2017-09-224-13/+13
* | Update the Cygwin x86-32 portXavier Leroy2017-09-121-10/+11
* | Resurrect the Cygwin x86-32 portXavier Leroy2017-09-111-2/+57
* | Print_annot should produce a string.Bernhard Schommer2017-07-191-3/+8
|/
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-065-11/+61
* Formatted json printing.Bernhard Schommer2017-06-282-3/+3
* Issues with invalid x86 addressing modes (Github issue #183)Xavier Leroy2017-05-173-18/+27
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-0315-90/+92
* RISC-V port and assorted changesXavier Leroy2017-04-282-0/+13
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-2/+4
* Use "Local" as prefixXavier Leroy2017-02-135-7/+7
* OS X: emit jumptables in .text segment, not .const segmentXavier Leroy2017-02-101-1/+1
* Inline open Datatypes.Bernhard Schommer2017-02-061-3/+2
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-8/+8
* Do not use hardcoded register number for sp.Bernhard Schommer2016-11-251-1/+1
* Use 64 bit address in debug information.Bernhard Schommer2016-11-101-0/+2
* x86: mark register rax as destroyed by callsXavier Leroy2016-11-081-1/+1
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-2727-0/+13205