aboutsummaryrefslogtreecommitdiffstats
path: root/backend/ValueDomain.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_divisionDavid Monniaux2021-12-141-2/+2
|\
| * Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-011-2/+2
| |\
| | * An improved PTree data structure (#420)Xavier Leroy2021-11-161-2/+2
* | | some more fixed etc. constructsDavid Monniaux2021-12-121-0/+156
|/ /
* | replacing omega with lia in some fileLéo Gourdin2021-03-291-2/+3
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-151/+156
|\|
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-10/+10
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-146/+146
* | risc-V now without trapping instructionsDavid Monniaux2020-09-211-0/+24
* | moved Risc-V div ValueAOp to central locationDavid Monniaux2020-09-211-0/+215
* | moved some "total" value domain functions to a central locationDavid Monniaux2020-09-211-1/+243
* | CSE2 alias analysis for Risc-VDavid Monniaux2020-03-031-5/+0
|/
* AArch64 portXavier Leroy2019-08-081-5/+26
* Perform constant propagation for known built-in functionsXavier Leroy2019-07-171-2/+42
* Support a "select" operation between two valuesXavier Leroy2019-05-201-0/+58
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-2/+2
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-2/+2
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-4/+4
* Issue #208: make value analysis of comparisons more conservative w.r.t. point...Xavier Leroy2017-11-241-8/+12
* 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
* | Remove coq warnings (#28)Bernhard Schommer2017-09-221-11/+11
|/
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-11/+24
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+17
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-1/+14
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-1/+17
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-114/+617
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-1/+1
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-221-0/+3
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-18/+36
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory...Xavier Leroy2016-05-071-111/+61
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-16/+8
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-389/+389
* ValueDomain: add some documentation comments.Xavier Leroy2015-07-191-20/+32
* Value analysis: keep track of pointer values that leak through small integers...Xavier Leroy2015-07-191-153/+171
* Value analysis: keep track of pointer values that leak through arithmetic ope...Xavier Leroy2015-07-191-152/+160
* ValueDomain.aptr_of_aval: be more conservative with pointers synthesized from...Xavier Leroy2015-07-181-5/+13
* Missing cases in ValueDomain.vnormalize, causing overapproximation.Xavier Leroy2015-07-181-2/+2
* Missing case in ValueDomain.pincl, causing incompleteness.Xavier Leroy2015-07-181-0/+9
* Introduce tolerance for casts of pointer values to/from 64-bit integers.Xavier Leroy2015-07-151-3/+12
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-3/+3
* Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-2/+4
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-4/+177
* Merge of "newspilling" branch:xleroy2014-07-231-84/+233
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-7/+4
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-091-0/+14
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-16/+13
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-5/+2
* 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-6/+4
generated by cgit (git 2.34.1) at 2024-05-09 13:40:34 +0000