CompCert

Kokeneet kirjoittajat eivät ole vielä tarkistaneet sivun nykyistä versiota, ja se voi poiketa merkittävästi 2. tammikuuta 2022 tarkistetusta versiosta . tarkastukset vaativat 2 muokkausta .
CompCert
Tyyppi Kääntäjä
Tekijä Xavier Leroy , INRIA
Sisään kirjoitettu Caml _ _
Ensimmäinen painos 3. huhtikuuta 2008
Laitteistoalusta Monialustainen ohjelmisto
uusin versio
Lisenssi ilmainen ei-kaupalliseen käyttöön [1] ; kaupalliset lisenssit AbsInt:ltä
Verkkosivusto compcert.inria.fr

CompCert on projekti, jolla luodaan virallisesti varmennettuja kääntäjiä. Projekti kehitti CompCert C -kääntäjän C - kielelle (ISO C90 / ANSI C -standardit pienin rajoituksin ja erillisillä laajennuksilla, jotka ovat inspiroituneet myöhemmistä standardeista), ja Coq -varmennusjärjestelmä oli täysin kirjoitettu ja esitelty . Pääkehittäjä on Xavier Leroy . Tällä kääntäjällä on konetarkistus, että luotu koodi käyttäytyy samalla tavalla kuin lähdekoodi. Kääntäjän avulla voit luoda konekoodia PowerPC- , ARM- ja x86 - suoritinarkkitehtuureille .

Motivaatio

Koska kääntäjät ovat erittäin monimutkaisia ​​ohjelmistoja, ne kärsivät usein monista virheistä [3] . He eivät esimerkiksi voi luoda koodia, joka vastaa lähdekoodia. Nämä virheet voivat johtaa erittäin vakaviin seurauksiin kriittisillä alueilla. Näin ollen CompCertin tavoitteena on luoda muodollisesti varmennettu kääntäjä, jolla on matemaattiset takuut.

Toteutus

CompCertin luoma koodi on noin kaksi kertaa nopeampi kuin ilman optimointia luotu GCC ja hieman hitaampi kuin korkeammalla optimointitasolla luotu koodi. [neljä]

Katso myös

Muistiinpanot

  1. ↑ Arkistoitu kopio . Haettu 12. joulukuuta 2016. Arkistoitu alkuperäisestä 13. elokuuta 2011.
  2. ↑ https://github.com/AbsInt/CompCert/releases/tag/v3.11
  3. ↑ Arkistoitu kopio . Haettu 12. joulukuuta 2016. Arkistoitu alkuperäisestä 6. heinäkuuta 2017.
  4. ↑ CompCert - CompCert C -kääntäjä . Käyttöpäivä: 12. joulukuuta 2016. Arkistoitu alkuperäisestä 3. joulukuuta 2015.

Linkit