CompCert

CompCert
Original author(s)Xavier Leroy
Developer(s)AbsInt
Initial release2005; 19 years ago (2005)
Stable release
3.15 / 13 December 2024[1]
Repository
TypeCompiler
Licensefree for noncommercial use[2]
Websitecompcert.org/compcert-C.html Edit this at Wikidata

CompCert is a formally verified optimizing compiler for a large subset of the C99 programming language (known as Clight) which currently targets PowerPC, ARM, RISC-V, x86 and x86-64[3] architectures.[4] This project, led by Xavier Leroy, started officially in 2005, funded by the French institutes ANR and INRIA. The compiler is specified, programmed and proven in Coq. It aims to be used for programming embedded systems requiring reliability. The performance of its generated code is often close to that of GCC (version 3) at optimization level -O1, and always better than that of GCC without optimizations.[5]

Since 2015, AbsInt offers commercial licenses,[6] provides support and maintenance, and contributes to the advancement of the tool. CompCert is released under a noncommercial license, and is therefore not free software, although some of its source files are dual-licensed with the GNU Lesser General Public License version 2.1 or later or are available under the terms of other licenses.[2]

For the development of CompCert, the first practically useful optimizing compiler targeting multiple commercial architectures that has a complete, mechanically checked proof of its correctness, Xavier Leroy and the development team of CompCert received the 2021 ACM Software System Award.

References

  1. ^ "Release Compcert 3.15". 13 December 2024. Retrieved 14 December 2024.
  2. ^ a b "CompCert License".
  3. ^ v3.0 Release Notes
  4. ^ CompCert Website
  5. ^ CompCert Performance
  6. ^ "CompCert - Partners". compcert.inria.fr. Retrieved 2019-03-21.


Stub icon

This programming-tool-related article is a stub. You can help Wikipedia by expanding it.

Read other articles:

Ōtsuki, Kōchi

Ōtsuki 大月町Kota kecil BenderaLambangLokasi Ōtsuki di Prefektur KōchiNegara JepangWilayahShikokuPrefektur KōchiDistrikHataPemerintahan • Wali kotaJun'ichi OkadaLuas • Total103 km2 (40 sq mi)Populasi (Oktober 1, 2015) • Total5.095 • Kepadatan49,47/km2 (12,810/sq mi)Zona waktuUTC+09:00 (JST)Kode pos788-0302Simbol  • PohonQuercus phillyraeoides • BungaCrinum asiaticum •&...

 

 

Frekuensi ultra tinggi

Pembagian dari Frekuensi radio : Frekuensi amat rendah - Frekuensi super rendah - Frekuensi ultra rendah - Frekuensi sangat rendah - Frekuensi rendah - Frekuensi sedang - Frekuensi tinggi - Frekuensi sangat tinggi - Frekuensi ultra tinggi - Frekuensi super tinggi - Frekuensi amat tinggi Pita radio ITU 1 (ELF) 2 (SLF) 3 (ULF) 4 (VLF) 5 (LF) 6 (MF) 7 (HF) 8 (VHF) 9 (UHF) 10 (SHF) 11 (EHF) 12 (THF) EU / NATO / US ECM A B C D E F G H I J K L M N IEEE HF VHF UHF L S C X Ku K Ka V W...

 

 

Finlandssvenska

Områden markerade med blå färg är de där den övervägande majoriteten av de svenskspråkiga i Finland bor. Finlandssvenska (finska: suomenruotsi) är en överregional varietet av svenska som är karakteristisk för finlandssvenskar och som kännetecknas av vissa finländska särdrag.[1] Inom finlandssvenskan finns ett flertal dialekter. De finlandssvenska dialekterna tillhör gruppen östsvenska mål till vilken även estlandssvenska hör. Svenska är ett av Finlands två nationalspråk...

Tujuan Pembangunan Berkelanjutan

Tujuan Pembangunan BerkelanjutanSustainable Development GoalsMisiSelembar cetak biru untuk mencapai masa depan yang lebih baik dan berkelanjutan untuk seluruh masyarakat dan dunia pada 2030.Jenis proyekOrganisasi nirlabaLokasiSeluruh duniaPemilikDidukung oleh Perserikatan Bangsa-Bangsa & dimiliki oleh masyarakatPendiriPerserikatan Bangsa-BangsaDimulai2015Situs websdgs.un.org Tujuan Pembangunan Berkelanjutan (bahasa Inggris: Sustainable Development Goals, disingkat SDGs atau Global Goals) ...

 

 

Kopling sentrifugal

Kopling lalu lintas dari mobil Talbot pada 1930 an Kopling sentrifugal atau sambatan mengempar adalah kopling dengan gaya sentrifugal untuk menghubungkan dua poros segaris, dengan poros pemutar ditempatkan di dalam poros yang diputar.[1] Input dari kopling dihubungkan dengan poros engkol mesin, sedangkan output-nya bisa menggerakan poros, rantai atau sabuk.[2] Thomas Fogarty, yang juga menemukan balloon catheter juga dianggap sebagai penemu kopling sentrifugal pada tahun 1940-...

 

 

Синелобый амазон

Синелобый амазон Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеНадкласс:ЧетвероногиеКлада:АмниотыКлада:ЗавропсидыКласс:Пт�...

Человек прямоходящий

† Человек прямоходящий Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеНадкласс:ЧетвероногиеКлада:АмниотыКлада:Синапсиды�...

 

 

Athens Metro rolling stock

Electric Multiple Units (EMU) are powered on the metro network of Athens, with five or six coaches. EMU-5s are of a former type and are limited to Line 1. On Lines 2 and 3, routes are only operated with EMU-6s. The trainsets were put into operation by STASY (Statheres Sygkoinonies) in 2011, with its establishment (previously operated from the companies ISAP S.A. for Line 1 and AMEL S.A. for Lines 2&3). Line 1 Historical stock Steam locomotives SAP (Athens-Piraeus Railway Company) In the ...

 

 

Rockabilly

RockabillyRockabillys im Tanzcafe LiBella, Altenmarkt an der AlzSumber aliranRock and rollcountrybluegrasswestern swingrhythm and bluesSumber kebudayaanAwal hingga pertengahan 1950-an, Amerika Serikat SelatanBentuk turunanGarage rockGenre campuran (fusion)PsychobillygothabillyTopik lainnya Country rock Rockabilly adalah salah satu gaya paling awal dan paling berpengaruh dalam musik rock n' roll yang muncul pada tahun 1950-an. Elvis Presley adalah bintang rockabilly yang paling terkenal. Walau...

羅德島州

本條目存在以下問題，請協助改善本條目或在討論頁針對議題發表看法。 此條目需要擴充。 (2013年1月1日)请協助改善这篇條目，更進一步的信息可能會在討論頁或扩充请求中找到。请在擴充條目後將此模板移除。 此條目需要补充更多来源。 (2013年1月1日)请协助補充多方面可靠来源以改善这篇条目，无法查证的内容可能會因為异议提出而被移除。致使用者：请搜索一下条目的...

 

 

Annunciation in Christian art

Subject in art The Virgin shrinks back in reluctance in the Annunciation with Sts. Margaret and Ansanus, by Simone Martini and Lippo Memmi, 1333 Aix Annunciation, generally attributed to Barthélemy d'Eyck, c. 1443–1445 Domenico Beccafumi, 1545 The Annunciation has been one of the most frequent subjects of Christian art.[1][2] Depictions of the Annunciation go back to early Christianity, with the Priscilla catacomb in Rome including the oldest known fresco of the Annunciatio...

 

 

منتخب جبل طارق للكريكت

منتخب جبل طارق للكريكت تعديل مصدري - تعديل   منتخب جبل طارق للكريكت هو ممثل جبل طارق الرسمي في المنافسات الدولية في الكريكت .[1][2][3] تشكيلة المنتخب قائمة اللاعبين مراجع ^ History of the Gibraltar Cricket Association. Gibraltar Cricket Association. مؤرشف من الأصل في 17 October 2007. اطلع عليه بتاريخ 20 Octo...

Keamari District

District of Sindh in PakistanKeamari District ضلع کیماڑیڪياماڙي ضلعو‎‎District of SindhTop: Keamari Boat TerminalBottom: Paradise PointCountry PakistanProvince SindhDivisionKarachiEstablished2020Headquarters[1]DMC Keamari officeGovernment[4] • TypeMunicipal corporation • BodyDMC Keamari • Deputy CommissionerMukhtiar Ali Abro[2] • AdministratorIqbal Ahmed Mirani[3]Area •...

 

 

Royal Marines

Maritime land warfare force of the United Kingdom For the racehorse, see Royal Marine (horse). Corps of Royal MarinesBadge of the Royal MarinesActive28 October 1664 – present(359 years, 7 months)Country United KingdomTypeMarines, Special operations-capable[1]Size5,820 as of 1 April 2022[update][2] 770 officers 5,050 other ranks Part of His Majesty's Naval ServiceUK Special Forces (1 Company, assigned to the SFSG)Naval staff officesWhiteh...

 

 

Momoka Ariyasu

Momoka AriyasuInformasi latar belakangNama lainMomokā~, Ariyasu~ (julukan)[1]Lahir15 Maret 1995 (umur 29)AsalPrefektur Saitama, Jepang[2]GenrePopPekerjaanPenyanyiTahun aktif1996-2018LabelKing RecordsArtis terkaitMomoiro Clover ZSitus webhttp://www.momoclo.net/ Momoka Ariyasu (有安 杏果code: ja is deprecated , Ariyasu Momoka, kelahiran 15 Maret 1995) adalah seorang mantan penyanyi idola Jepang. Ia dikenal sebagai seorang anggota dari grup musik khusus perempuan Momoir...

Serie A1 1996-1997 (pallavolo maschile)

La Serie A1 maschile FIPAV 1996-97 fu la 52ª edizione della manifestazione pallavolistica organizzata dalla FIPAV. La regular season si svolse tra il 29 settembre 1996 e il 16 marzo 1997. Indice 1 Regolamento 2 Avvenimenti 3 Le squadre partecipanti 4 Classifica 5 Risultati 5.1 Tabellone 5.2 Calendario 6 Play-off Scudetto 7 Fonti Regolamento Le 12 squadre partecipanti disputarono un girone unico con partite di andata e ritorno, cui fecero seguito i play-off scudetto, ai quali presero parte, a...

 

 

1/4 + 1/16 + 1/64 + 1/256 + ⋯

Infinite sum equal to 1/3 at its limit Archimedes' figure with a = 3/4 In mathematics, the infinite series 1/4 + 1/16 + 1/64 + 1/256 + ⋯ is an example of one of the first infinite series to be summed in the history of mathematics; it was used by Archimedes circa 250–200 BC.[1] As it is a geometric series with first term 1/4 and common ratio 1/4, its sum is ∑ n = 1 ∞ 1 4 n = 1 4 1 − 1 4 = 1 3 . {\displaystyle \sum _{n=1}^{\infty }{\frac {1}{4^{n}...

 

 

1994年冬季奧林匹克運動會安道爾代表團

1994年冬季奥林匹克运动会安道尔代表團安道尔国旗IOC編碼ANDNOC安道爾奧林匹克委員會網站www.coa.ad（加泰罗尼亚文）1994年冬季奥林匹克运动会（利勒哈默尔）1994年2月12日至2月27日運動員6 (4男2女)參賽項目1个大项旗手Vicky Grau獎牌榜 金牌 銀牌 銅牌 總計 0 0 0 0 历届奥林匹克运动会参赛记录（总结）夏季奥林匹克运动会1976198019841988199219962000200420082012201620202024冬季奥林匹克运动会...

Stepanakert

City in Karabakh, Azerbaijan Xankəndi redirects here. For other uses, see Xankəndi (disambiguation). Parts of this article (those related to the Artsakh era) need to be updated. Please help update this article to reflect recent events or newly available information. (October 2023) City in Karabakh, AzerbaijanStepanakert / Khankendi ՍտեփանակերտXankəndiCityFrom top left: Holy Mother of God Cathedral Renaissance Square • Downtown Stepanakert Stepanakert Airport • Step...

 

 

Cotswold architecture

Architectural design style Cotswold ArchitectureCotswold Cottage, Coln St. AldwynsLocationEngland, United StatesInfluencesClassical architecture, Tudor Revival The Cotswold style of architecture is a style based on houses from the Cotswold region of England. Cotswold houses often have a prominent chimney, often near the front door of the house.[1] Other notable features include king mullions and steep roofs. The Cotswold style uses local materials based on geology. This style is renow...