aboutsummaryrefslogtreecommitdiffstats
path: root/midend
Commit message (Expand)AuthorAgeFilesLines
* one problem in this file (admitted)David Monniaux2021-01-101-2/+2
* Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssaDavid Monniaux2021-01-081-0/+482
* Merge remote-tracking branch 'compcertssa/issue1' into kvx-work-ssaDavid Monniaux2020-11-054-42/+79
|\
| * generalize entrypoint normalization checker + low-cost error messagesDelphine Demange2020-11-052-33/+70
| * low-cost error messagesDelphine Demange2020-11-051-7/+7
| * low-cost error messagesDelphine Demange2020-11-051-2/+2
* | no more admittedDavid Monniaux2020-07-201-2/+2
* | remove some 'Admitted'David Monniaux2020-07-203-5/+31
* | no more admit in RTLnormproofDavid Monniaux2020-07-201-9/+22
* | notrap caes in SSAvalidproofDavid Monniaux2020-07-201-0/+29
* | rm admittedDavid Monniaux2020-07-201-3/+47
* | one less admittedDavid Monniaux2020-07-201-3/+43
* | more on RTLparDavid Monniaux2020-07-202-0/+45
* | notrap in RTLparproofDavid Monniaux2020-07-201-0/+146
* | some more notrap casesDavid Monniaux2020-07-201-0/+36
* | two more casesDavid Monniaux2020-07-201-0/+54
* | one less admittedDavid Monniaux2020-07-202-3/+64
* | one less 'admitted'David Monniaux2020-07-201-3/+15
* | one less 'admitted'David Monniaux2020-07-201-3/+11
* | added NOTRAP to SSA semantics, now lots of 'admitted'David Monniaux2020-07-206-6/+51
* | compile with "admitteds" wrt loadsDavid Monniaux2020-07-1710-57/+70
* | Iload and Icond are now slightly differentDavid Monniaux2020-07-1727-152/+153
|/
* minor cosmetic changes in SSA fileDelphine Demange2020-07-116-49/+37
* minor cosmetic changes in SSA fileDelphine Demange2020-07-1010-642/+546
* Remove some unused lemmasDelphine Demange2020-07-081-385/+0
* Moving validator spec in the right fileDelphine Demange2020-07-082-230/+229
* Reduce compilation time of validator proofDelphine Demange2020-07-081-102/+130
* Global renaming of files in the middle-endDelphine Demange2020-07-0835-1128/+1121
* Cleaning commented-out lemmaDelphine Demange2020-07-071-21/+0
* Global cleanup of code base.Delphine Demange2020-07-0747-3417/+793
* Use CompCert's Maps interface.Delphine Demange2020-07-056-3324/+1
* Reuse of RTL pretting printerDelphine Demange2020-07-051-34/+3
* Performance improvement in computation of coalescing classes.Delphine Demange2020-07-051-153/+57
* SCCP optimization support for all architectures, with reuse ofDelphine Demange2020-07-0311-828/+3167
* SSA registers are no longer indexed by positives, but just raw positives.Delphine Demange2020-07-0141-3693/+4066
* Removing old filesDelphine Demange2020-07-017-4212/+0
* Cleaning traces of old (naive) SSA destruction.Delphine Demange2020-06-227-2566/+8
* Fixing warnings and proof checking errors related to hint databases.DEMANGE Delphine2020-06-1835-228/+240
* Merge tag 'v3.6' into ssaDEMANGE Delphine2020-06-177-10/+68
* Fix some extraction warning by making some definition transparentDEMANGE Delphine2020-06-173-5/+5
* Removes warnings related to deprecated definitions and practicesDEMANGE Delphine2020-06-1717-113/+106
* Delete irrelevant filesDEMANGE Delphine2020-06-171-126/+0
* Merge tag 'v3.4' into ssaDEMANGE Delphine2020-06-166-28/+25
* SSA middle-end for compcert v3.2DEMANGE Delphine2020-06-1285-0/+62679
generated by cgit (git 2.34.1) at 2024-06-02 12:21:07 +0000