aboutsummaryrefslogtreecommitdiffstats
path: root/backend/ValueAnalysis.v
Commit message (Expand)AuthorAgeFilesLines
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-11/+4
* Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-181-2/+0
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-13/+13
|\
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-2/+2
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-11/+11
* | Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-1/+1
* | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-031-3/+2
|\|
| * Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-3/+2
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-12-091-4/+27
|\ \ | |/ |/|
| * begin CSEDavid Monniaux2019-09-041-0/+3
| * Value analysis for non trapping loadsDavid Monniaux2019-09-031-4/+24
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-031-1/+51
| |\
| * | avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-1/+1
* | | Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-021-4/+4
| |/ |/|
* | Perform constant propagation for known built-in functionsXavier Leroy2019-07-171-1/+51
|/
* ValueAnalysis: remove duplicate list_forall2_in_left (#212)Jérémie Koenig2018-01-031-13/+2
* 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-191-2/+2
* | Remove coq warnings (#28)Bernhard Schommer2017-09-221-2/+2
|/
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-0/+5
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-8/+8
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-18/+22
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-102/+147
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-314/+314
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-1/+1
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-153/+251
* Value analysis: keep track of pointer values that leak through arithmetic ope...Xavier Leroy2015-07-191-4/+4
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-1/+1
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-11/+7
* Merge branch 'named-structs'Xavier Leroy2015-01-231-1/+1
|\
| * Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-261-1/+1
* | Follow-up to [5aecefe]: be conservative also in the case of a "common" global...Xavier Leroy2015-01-201-6/+21
* | More prudent analysis of uninitialized const global variables.Xavier Leroy2015-01-091-3/+6
|/
* Merge of "newspilling" branch:xleroy2014-07-231-2/+2
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-3/+4
* Updated ARM backend wrt new static analyses and optimizations.xleroy2014-01-021-0/+12
* Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).xleroy2013-12-301-3/+0
* Merge of branch value-analysis.xleroy2013-12-201-0/+1812
generated by cgit (git 2.34.1) at 2024-05-09 09:59:15 +0000