Polyspace Code Prover

범위 정보 보기

Polyspace Code Prover는 소프트웨어를 통해 제어와 데이터 흐름을 추적하고 변수 및 연산자와 연결된 범위 정보를 표시합니다. 커서를 연산자 또는 변수 위에 올려놓으면 툴팁 메시지가 범위 정보를 표시합니다. 추상적 해석(abstract interpretation)으로 알려진 정형 기법(formal method)은 정확한 범위 정보의 측정으로 소프트웨어에 특정 런타임 오류가 없음을 증명하기 위한 목적을 달성하도록 합니다. 범위 정보를 사용하여 소프트웨어를 디버깅하거나 특정 변수 또는 연산이 지정된 범위 한도를 위반하지 않았다는 것을 확실하게 알 수 있습니다.

아래 예제에서 Polyspace Code Prover는 나누기 연산의 왼쪽 피연산자가 -1701~3276의 범위이고 오른쪽 피연산자가 9임을 파악했습니다. 나누기 후 결과 범위는 -189~364입니다.

Tooltip displaying the possible ranges for all run time conditions.
모든 런타임 조건에 대한 가능한 범위를 표시하는 툴팁

호출 계층과 호출 흐름 그래프를 사용하여 제어 흐름을 추가적으로 시각화할 수 있습니다.

Call flow graph displaying the order of function calls in an interprocedural analysis.
절차적 분석에서 함수 호출 순서
다음: 소프트웨어 품질 메트릭 추적

평가판 사용 Polyspace Code Prover

평가판 신청

Comprehensive Static Analysis Using Polyspace Products

온라인 세미나 보기