aboutsummaryrefslogtreecommitdiffstats
path: root/backend/SplitLongproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-15/+15
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-15/+15
* | various fixesDavid Monniaux2019-07-191-20/+0
* | helpers broke compilationDavid Monniaux2019-07-191-6/+0
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-41/+89
|\|
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-72/+61
* | ça recompile sur x86David Monniaux2019-03-221-1/+2
* | Proving eval_divs_baseCyril SIX2019-03-201-1/+1
* | added helper functions but strangeDavid Monniaux2019-03-191-51/+0
|/
* Prefixed runtime functions.Bernhard Schommer2017-08-251-30/+30
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-10/+10
* Use "Local" as prefixXavier Leroy2017-02-131-2/+2
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-6/+6
* SplitLong: propagate constants through "longofint"Xavier Leroy2016-10-251-2/+3
* Update ARM port. Not tested yet.Xavier Leroy2016-10-251-1/+1
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-2/+20
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+1
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-86/+47
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-0/+1142
generated by cgit (git 2.34.1) at 2024-05-09 08:48:24 +0000