aboutsummaryrefslogtreecommitdiffstats
path: root/common/Values.v
Commit message (Expand)AuthorAgeFilesLines
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-5/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-17/+17
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-1/+32
* Relax lemma Val.zero_ext_and and add Val.zero_ext_andlXavier Leroy2019-08-071-2/+10
* Values: add functions for zero- and sign-extension of 64-bit integersXavier Leroy2019-08-071-0/+12
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-5/+5
* Support a "select" operation between two valuesXavier Leroy2019-05-201-0/+126
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+34
* Constprop strength reduction (#17)Bernhard Schommer2017-07-121-0/+21
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-22/+71
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+12
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+100
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-132/+580
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-4/+7
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-73/+73
* Typo: Val.sun_inject -> Val.sub_inject.Xavier Leroy2015-05-061-1/+1
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-57/+59
* Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-011-0/+6
|\
| * Extended arguments to annotations, continued:Xavier Leroy2015-03-271-0/+6
* | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-17/+33
|/
* Merge of "newspilling" branch:xleroy2014-07-231-17/+122
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-1/+1
* Merge of branch value-analysis.xleroy2013-12-201-0/+6
* Merge of Flocq version 2.2.0.xleroy2013-08-021-5/+0
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+12
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-0/+12
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+12
* Merge of the "princeton" branch:xleroy2013-06-161-15/+15
* Merge of the float32 branch: xleroy2013-05-191-7/+38
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-4/+4
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-10/+252
* Pointers one pastxleroy2013-02-151-18/+149
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-6/+6
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-5/+5
* Updated documentationv1.12xleroy2013-01-111-1/+1
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-67/+62
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-1/+24
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-4/+12
* Hack with nxorxleroy2012-05-181-0/+5
* Merge of the "volatile" branch:xleroy2012-02-041-0/+7
* Merge of the nonstrict-ops branch:xleroy2012-01-141-221/+284
* Back from Oregon commit. xleroy2011-07-051-0/+6
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-2/+2
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+6
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-0/+8
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+81
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-21/+17
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-2/+2
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-261-0/+17
generated by cgit (git 2.34.1) at 2024-06-02 23:45:56 +0000