aboutsummaryrefslogtreecommitdiffstats
path: root/arm/ConstpropOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-171-1/+25
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-161-9/+31
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-051-0/+8
* Strength reduction patterns for ARM mla instruction.Gergö Barany2017-09-151-0/+73
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-1/+1
* Update ARM port. Not tested yet.Xavier Leroy2016-10-251-36/+62
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-1/+1
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-66/+66
* Value analysis: keep track of pointer values that leak through small integers...Xavier Leroy2015-07-191-14/+14
* Merge of "newspilling" branch:xleroy2014-07-231-19/+49
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-2/+2
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-091-3/+47
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-0/+1
* Updated ARM backend wrt new static analyses and optimizations.xleroy2014-01-021-237/+205
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-141-0/+32
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-1/+4
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-241-13/+0
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-8/+8
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-1/+2
* Merge of the newmem branch:xleroy2012-05-211-2/+24
* Support for fcmpzd instruction (float compare with +0.0)xleroy2012-03-291-0/+9
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-151-0/+14
* Merge of the nonstrict-ops branch:xleroy2012-01-141-358/+245
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-0/+2
* Merge of branch "unsigned-offsets":xleroy2011-04-091-55/+56
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-0/+2
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+1
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-8/+8
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-181-11/+0
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-171-0/+541
generated by cgit (git 2.34.1) at 2024-05-08 10:00:30 +0000