aboutsummaryrefslogtreecommitdiffstats
path: root/common/Values.v
Commit message (Expand)AuthorAgeFilesLines
* Values: conversions to nearest intDavid Monniaux2021-12-121-0/+48
* remove todos, cleanLéo Gourdin2021-07-281-0/+14
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* replacing omega with lia in some fileLéo Gourdin2021-03-291-6/+7
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-22/+22
|\
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-5/+5
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-17/+17
* | has_type_bDavid Monniaux2021-01-301-0/+21
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-0/+49
* | missing lemmasDavid Monniaux2020-11-251-0/+21
* | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-031-0/+106
|\ \ | |/ |/|
| * shrxl_shrl_3David Monniaux2020-01-141-0/+52
| * shrx_shr_3David Monniaux2020-01-141-0/+54
* | 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
generated by cgit (git 2.34.1) at 2024-05-09 18:06:13 +0000