값 대신 경로 조건
일반 실행에서는 하나의 숫자를 넣어 분기를 선택한다. 기호 실행에서는 분기에 진입하는 조건을 쌓아 어떤 입력에서 그 경로가 가능한지 분석한다. SPF는 기본형 인자를 받는 메서드를 다루며 문자열, 배열, 사용자 정의 자료구조에 대한 지원도 제공한다.
구체 실행과 결합
symcrete 모드에서는 구체적인 입력으로 경로를 실행하면서 그 경로의 제약을 수집한다. 실행 결과만 기록하는 테스트와 달리 입력과 분기 사이의 조건을 함께 살펴볼 수 있다. 분석 가능한 기능과 설정은 대상 프로그램에 맞춰 확인해야 한다.
호환성 주의
확장 저장소의 설치 안내는 자바 8과 특정 jpf-core 조합을 제시한다. 최신 JPF 코어의 요구 사항과 동일하다고 가정하면 설치부터 어긋날 수 있다. 재현 가능한 분석을 위해 두 프로젝트의 버전과 해결기 환경을 함께 고정하는 편이 좋다.
관련 문서
Java PathFinder / Angr / S2E / TritonDSE