aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Constpropproof.v
Commit message (Expand)AuthorAgeFilesLines
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-76/+75
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-2/+2
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-2/+2
* | Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-2/+2
* | fixes for compiling on other platformsDavid Monniaux2019-09-071-2/+2
* | fixes for ARMDavid Monniaux2019-09-071-8/+4
* | notrap works on x86David Monniaux2019-09-071-12/+3
* | more for passing notrap through x86David Monniaux2019-09-071-2/+10
* | finished Constopproof for non trapping loadsDavid Monniaux2019-09-031-1/+41
* | advancing in constant propagationDavid Monniaux2019-09-031-0/+20
|/
* Perform constant propagation for known built-in functionsXavier Leroy2019-07-171-11/+33
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-2/+2
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-10/+10
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-28/+14
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-141/+123
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-64/+64
* Experiment: track the scopes of local variables via __builtin_debug.Xavier Leroy2015-09-201-1/+5
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-72/+64
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-58/+46
* Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-261-2/+2
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-3/+10
* Merge of "newspilling" branch:xleroy2014-07-231-0/+2
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-3/+3
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-2/+3
* Merge of branch value-analysis.xleroy2013-12-201-541/+241
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-141-4/+8
* Simplify LPMap by smashing bottoms.xleroy2013-08-121-7/+8
* Change interface of Kildall solvers to avoid precomputing the map pc -> list ...xleroy2013-08-121-3/+2
* Merge of the "princeton" branch:xleroy2013-06-161-5/+5
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+5
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-9/+24
* Constant propagation within __builtin_annot.xleroy2013-02-241-5/+69
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-10/+10
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-13/+16
* More aggressive elimination of conditional branches during constantxleroy2012-08-011-194/+182
* Merge of the newmem branch:xleroy2012-05-211-86/+410
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-151-3/+7
* Merge of the nonstrict-ops branch:xleroy2012-01-141-131/+183
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-6/+4
* Merge of branch "unsigned-offsets":xleroy2011-04-091-9/+9
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...xleroy2010-10-271-1/+1
* Support for inlined built-ins.xleroy2010-06-291-0/+11
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+9
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-0/+1
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-30/+27
* Added support for jump tables in back end.xleroy2009-11-101-0/+12
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-181-0/+11
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-171-0/+445
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-954/+0
generated by cgit (git 2.34.1) at 2024-05-09 05:40:06 +0000