aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Integers.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-2/+114
|\
| * Native support for bit fields (#400)Xavier Leroy2021-08-221-0/+112
| * Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* | coq 8.13.2David Monniaux2021-06-071-2/+1
* | [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-20/+21
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-542/+545
|\|
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-22/+25
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-520/+520
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-1/+178
|\ \
| * | shrx'1_shr'David Monniaux2020-01-141-1/+127
| * | shrx1_shrDavid Monniaux2020-01-141-0/+51
| |/
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-11-131-4/+5
|\|
| * More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
* | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-161-37/+416
|\|
| * AArch64 portXavier Leroy2019-08-081-24/+136
| * Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
| * Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
| * Define integer sign extension for zero bitsXavier Leroy2019-08-071-14/+27
* | IcondCyril SIX2019-10-071-0/+5
* | Ibuiltin proofCyril SIX2019-10-041-11/+27
* | Adding decidable equality for intCyril SIX2019-10-041-1/+12
|/
* More efficient test for powers of twoXavier Leroy2019-05-091-26/+22
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-835/+33
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-10/+10
* Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
* Make the checker happy (#272)Vincent Laporte2019-02-121-8/+8
* Removed deprecated lemma.Bernhard Schommer2018-03-121-1/+1
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+6
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-57/+57
* Some lemmas.Bernhard Schommer2017-09-211-0/+14
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-43/+134
* RISC-V port and assorted changesXavier Leroy2017-04-281-3/+23
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+108
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+37
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+454
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-181-0/+92
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-4/+4
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-618/+618
* Tweaks to support defunctorization.xleroy2014-07-231-9/+19
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-091-0/+10
* Merge of branch value-analysis.xleroy2013-12-201-0/+13
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+28
* Add another expansion of shrx in terms of shifts and adds (from Hacker's Deli...xleroy2013-07-281-42/+72
* More properties about subtraction and borrow.xleroy2013-07-151-18/+59
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-8/+119
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-35/+59
* Decomposing 64-bit "less than" comparisons.xleroy2013-04-291-9/+70
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-34/+430
generated by cgit (git 2.34.1) at 2024-05-09 09:45:15 +0000