CompCert

CompCert
CompCert
원본 작성자사비에 르로이
개발자압신트
초기 릴리즈2005; 17년 전(2005)
안정적 해제
3.10 / 2021년 11월 19일; 2개월 전(2021-11-19)
리포지토리
유형컴파일러
면허증비상업적인 용도로[1] 무료.
웹사이트compcert.org/compcert-C.html Edit this at Wikidata

CompCert는 현재 PowerPC, ARM, RISC-V, x86 및 x86-64[2] 아키텍처를 대상으로 하는 C99 프로그래밍 언어(일명 클라이트)의 대규모 서브셋에 대해 컴파일러 최적화를 공식적으로 검증한 것이다.[3] 자비에 르로이가 주도한 이 프로젝트는 프랑스 연구소 ANR와 INRIA가 자금을 지원받아 2005년 공식 시작됐다. 컴파일러는 Coq에서 지정, 프로그래밍 및 입증된다. 신뢰성이 요구되는 임베디드 시스템을 프로그래밍하는 데 사용하는 것을 목표로 한다. 생성된 코드의 성능은 최적화 수준 -O1에서 GCC(버전 3)에 근접한 경우가 많으며, 최적화가 없는 GCC보다 항상 우수하다.[4]

2015년 이후 복근Int는 상용 라이선스를 제공하고,[5] 지원과 유지보수를 제공하며, 툴의 발전에 기여한다. CompCert는 비상업용 라이센스로 출시되며, 따라서 일부 소스 파일은 GNU 소일반 공중 라이센스 버전 2.1 이상으로 이중 라이센스가 부여되거나 다른 라이센스의 조건에 따라 사용할 수 있지만 무료 소프트웨어가 아니다.[1]

참조

  1. ^ a b "CompCert License".
  2. ^ v3.0 릴리스 정보
  3. ^ CompCert 웹 사이트
  4. ^ CompCert 성능
  5. ^ "CompCert - Partners". compcert.inria.fr. Retrieved 2019-03-21.

외부 링크

Stub icon

이 소프트웨어 기사는 엉터리야. 위키피디아를 확장하여 도울 수 있다.