aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-1/+1
|\
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-1/+1
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-9/+9
|\|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-9/+9
* | add has_type infoDavid Monniaux2021-01-311-1/+3
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-41/+43
|\|
| * Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+4
| * Eliminate known builtins whose result is ignoredXavier Leroy2020-06-251-34/+39
* | __builtin_expect seems to workDavid Monniaux2020-04-071-3/+3
* | start implementing expect as exprDavid Monniaux2020-04-071-42/+43
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-expectDavid Monniaux2020-04-061-2/+2
|\ \
| * | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-201-2/+2
| |\|
| | * AArch64 portXavier Leroy2019-08-081-2/+2
* | | __builtin_expect defined as its first argumentDavid Monniaux2019-09-251-0/+7
|/ /
* | various fixesDavid Monniaux2019-07-191-3/+3
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-36/+125
|\|
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-34/+123
| * If-conversion optimizationXavier Leroy2019-06-061-63/+323
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-031-67/+327
|\ \
| * | If-conversion optimizationXavier Leroy2019-05-311-63/+323
| |/
| * lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-1/+1
| * Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
* | itemize the proof (better for debugging)David Monniaux2019-04-051-10/+10
* | removed the unproved hack to get builtins, will be reinstated laterDavid Monniaux2019-04-051-6/+0
* | some more on builtinsDavid Monniaux2019-04-031-0/+6
* | ça recompile sur x86David Monniaux2019-03-221-0/+1
* | Proof of div32/mod32/divf32/divf64 lemmasCyril SIX2019-03-201-3/+3
|/
* 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-3/+3
|/
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-25/+38
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-2/+2
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-100/+57
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-2/+2
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-231/+329
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-118/+118
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-52/+110
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-55/+38
* Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-011-2/+71
|\
| * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-5/+26
| * Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-2/+50
* | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-1/+1
|/
* Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-201-57/+57
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-6/+12
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-123/+336
* Merge of "newspilling" branch:xleroy2014-07-231-0/+15
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-1/+1
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+2
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+2
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-19/+13
generated by cgit (git 2.34.1) at 2024-05-09 07:09:46 +0000