여러 분석을 결합하는 구조
하나의 방법으로 모든 오류를 확인하기는 어렵다. Frama-C는 분석 도구가 결과를 공유하도록 구성해 실행 오류 가능성과 명세 준수 여부를 여러 관점에서 살핀다. 어떤 플러그인을 어떤 설정으로 사용했는지가 결과의 범위를 결정한다. 플랫폼을 실행했다는 사실과 필요한 성질을 확인했다는 사실을 구분한다.
값 분석과 계약 증명
Eva는 추상 해석으로 가능한 값과 동작을 보수적으로 분석하고 지원하는 종류의 실행 오류에 대해 경고한다. WP는 전제조건과 사후조건 및 루프 불변식 같은 주석에서 검증 조건을 만든다. 안전성 조건과 함수가 원하는 값을 반환한다는 기능 명세는 다르므로 확인하려는 성질을 적절히 표현해야 한다.
정적 결과와 실행 중 확인
E-ACSL은 실행 가능한 명세 주석을 C 검사 코드로 바꾸어 실제 실행 중 확인한다. 이 결과는 관찰한 실행에 해당하며 가능한 모든 실행의 정적 보증과 같지 않다. 분석이 남긴 경고나 해결되지 않은 조건을 조사하는 데 함께 활용할 수 있다. 명세와 외부 환경의 가정 및 분석 설정을 보존해 보증 범위를 분명히 한다.