6
C 프로그램에서 불변량을 정적으로 발견 할 수있는 도구를 찾고 있습니다. 나는 Daikon을 체크 아웃했지만 invariants는 동적으로 만 발견합니다.C 프로그램에 대한 정적 불변 검색 도구가 있습니까?
내가 찾고있는 자료에 사용할 수있는 도구가 있습니까? 감사!
A
답변
4
Daikon에 대한 링크 된 페이지가 사용하고있는 가장 넓은 의미에서 "불변"을 의미하는 경우, 많은 정적 분석 도구의 작업은 찾고있는 표현형이 아닌 "불변 식 발견"이라고 할 수 있습니다 에 대한.
Frama-C의 가치 분석은 각 결과에 대해 모든 변수의 가능한 값인 결과를 누적합니다. 분석이 끝나면 각 변수에서 프로그램의 각 변수의 도메인 변수에 대한 비 관계형 정보를 표시 할 수 있습니다. this screenshot에서 불변 식은이 결정 성있는 프로그램의 모든 실행에 대해 S이 선택한 명령 직전에 항상 0, 1, 3 또는 6임을 나타냅니다.
질문에 숨겨진 두 매개 변수는 관심이있는 불변의 모양과 이러한 불변의 것을 찾으려는 프로그램의 모양입니다. 예를 들어, Ira의 답변에서 언급 한 SLAM은 장치 드라이버 코드에서 작동하고 시스템 API의 올바른 사용을 확인하는 데 필요한 정보 만 포함하는 불변 조건을 유추하도록 설계되었습니다. 다른 도구 인 Astrée은 비행 제어 소프트웨어의 런타임 안전성을 보여주기 위해 올바른 불변량을 유추하는 데 매우 유익한 일을하는 것으로 유명합니다.
두 자유도는 매우 큰 디자인 공간을 만듭니다. 모든 종류의 C 프로그램에서 작동하는 것을 찾지는 못하고 관심있는 모든 불변량을 유추하지만 특정 응용 프로그램 도메인과 불변량의 종류에 대해 질문을 수정하면 관련 답변을 찾을 수있는 기회가 더 많아집니다.
5
The SLAM project: debugging system software via static analysis을 참조하십시오. 그것은 invariant를 정적으로, 당신이 요구 한 것, C 언어에 대해서 유추한다고 주장합니다. 저자 인 Tom Ball은 프로그램 분석에서 탁월한 업적으로 널리 알려져 있습니다.
안녕하세요, 귀하의 회신에 감사드립니다. 나는 간격 (상자)과 같은 간단한 구조로 불변량에 흥미가 있습니다. 나는 Frama-C의 가치 분석이 단지 간격이 아닌 특정 값을 제공하기 때문에 더 낫다고 생각한다. –
@VijayaraghavanMurali 음, 어떤 정보를 버릴 지에 대한 모든 절충안이 있습니다. 예를 들어 Frama-C의 가치 분석은 값 집합을 최대 8 개의 요소로 유지 한 다음 합동 정보가있는 간격으로 전환합니다. 이것은 정수를위한 것입니다. 'float'과'double'의 경우, 개별적인 의미를 가진 신중한 값을 나타 내기 위해 자주 사용되지 않는다는 사실을 반영하기 위해 interval을 사용합니다. 주소는 http://frama-c.com/download/frama-c-value-analysis.pdf에 있습니다. –