에클레어

ECLAIR
에클레어
개발자BUGSENG, LLC
안정된 릴리스
3.12.0 / 2022년 2월 28일, 3개월 전(2022-02-28)[1]
운영 체제크로스 플랫폼
유형정적 코드 분석
면허증.독자 사양
웹 사이트www.bugseng.com/eclair

ECLAIR는 BUGSENG, LLC에 의해 개발된 상용 정적 코드 분석 도구로서 C 및 C++ 프로그램의 자동 분석, 검증, 테스트 및 변환을 위해 개발되었습니다.

기능

ECLAIR는 파르마 대학의 Applied Formal Methods Laboratory에서 개발된 일련의 프로토타입의[2] 완전한 리엔지니어링입니다.소스 코드에 특정 런타임 오류가 없음을 검출 또는 증명하기 위해 추상 해석모델 검사와 같은 공식 방법 기반 정적 코드 분석 기술을 사용하고 프로그램 분석 및 검증, 프로그램 테스트 생성 및 프로그램 변환을 지원합니다.

프로그램 분석 및 검증과 관련해서, ECLAIR 정정 또는 증명해 런타임 이상 징후를 부재뿐만 아니라 MISRA C, MISRA C++, 컴퓨터 침해 사고 대응반 C보안 코딩 표준 컴퓨터 침해 사고 대응반 C++보안 코딩 Standard,[3]High-Integrity C++, NASA/JPL C, ESA/BSSC C/C++, 같은 몇가지 코딩 표준에 대해 존경을 준수할 자동으로 확인할 수 있다. JSFC++, EC--,[4] Netrino Embedded C,[5] The Power of Ten(C),[6] Industrial Strength C++.[7]

프로그램 테스트의 경우 ECLAIR는 사용자가 지정한 적용 범위 기준에 도달하는 단위 테스트 입력 세트를 자동으로 합성하여 프로그램의 실행 불가능한 조건으로 인해 이 적용범위에 도달할 수 없을 때 사용자에게 경고할 수 있다.

프로그램 변환과 관련하여 ECLAIR를 사용하여 복잡한 프로그램 변환을 수행할 수 있습니다. ECLAIR는 구문 및 의미 기반 기준에 따라 지정됩니다. 이러한 기준과 일치하는 소스 내의 프로그램 영역을 매개 변수화된 대체로 선택적으로 대체할 수 있습니다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ "News - BUGSENG". bugseng.com. Retrieved 2021-04-04.
  2. ^ R. Bagnara; P. M. Hill; E. Zaffanella (2007). "A Prolog-based Environment for Reasoning about Programming Languages". arXiv:0711.0345 [cs.PL].
  3. ^ Seacord, Robert C. (2013). Secure Coding in C and C++. SEI Series in Software Engineering (2nd ed.). Addison-Wesley Professional. ISBN 978-0-321-82213-0.
  4. ^ Hatton, L. (2005). "EC—a measurement based safer subset of ISO C suitable for embedded system development". Information and Software Technology. 47 (3): 181–695. CiteSeerX 10.1.1.101.7828. doi:10.1016/j.infsof.2004.08.001.
  5. ^ Barr, Michael (2008). Embedded C Coding Standard. Barr Group. ISBN 978-1442164826.
  6. ^ Gerald, J. (2006). "The Power of 10: Rules for Developing Safety-Critical Code". Computer. 39 (6): 95–97. doi:10.1109/MC.2006.212.
  7. ^ Henricson, Mats; Nyquist, Erik (1997). Industrial Strength C++. Prentice-Hall PTR. ISBN 978-0131209657.

외부 링크