Polyspace Code Prover

런타임 오류 검출

Polyspace Code Prover는 정적 코드 분석(static analysis)과 추상적 해석(abstract interpretation)을 사용하여 오버플로우, 0으로 나누기 및 경계 밖 포인터와 같은 런타임 오류를 증명, 식별 및 진단할 수 있습니다. 이 기술은 모든 런타임 조건을 완벽하하게 포괄적으로 검증하며 자동으로 각 코드 연산에 대해 검증 여부, 실패 여부, 또는 도달 가능 여부 에 대한 진단을 제공합니다. Polyspace Code Prover가 생성한 검증 결과에서 각 C 또는 C++ 연산은 다음 색상 코드를 통해 상태를 나타냅니다.

녹색: 런타임 오류가 없는 것으로 증명됨
빨간색: 연산을 실행할 때마다 오류가 있음이 증명됨
회색: 도달할 수 없는 것으로 증명됨(기능 문제가 있을 수 있음)
오렌지색: 특정 조건에서 증명되지 않은 연산은 오류를 일으킬 수 있음

Color-coded run-time error attributes identified by Polyspace Code Prover.

Polyspace Code Prover에서 식별된 런타임 오류 속성

검출된 오류:

  • 오버플로우, 언더플로우, 0으로 나누기 및 기타 산술 오류
  • 경계 밖 배열 액세스 및 잘못 참조 해제된 포인터
  • 항상 true 또는 false인 구문
  • 초기화되지 않은 클래스 멤버(C++)
  • 초기화되지 않은 데이터에 대한 읽기 액세스
  • Null this포인터에 대한 액세스(C++)
  • 데드 코드(dead code)
  • 객체 프로그래밍, 상속 및 예외 처리(C++)와 관련된 동적 오류
다음: 범위 정보 보기

평가판 사용 Polyspace Code Prover

평가판 신청

Comprehensive Static Analysis Using Polyspace Products

온라인 세미나 보기