Ubuntu 14.04에서 Frama-c 용 Impact Analysis 플러그인을 설치하는 방법은 무엇입니까? 그러나</p> <pre><code>sudo apt-get install frama-c </code></pre> <p>, 나는 다음과 같은 명령을 사용하여 FRAMA-C의 GUI를 열 때 :</p> <pre><code>frama-c-gui </code></pre> <p>나는를 찾을 수 없습니다

Question

나는 다음과 같은 명령을 사용하여, 우분투 14.04에 FRAMA-C를 설치 왼쪽 창에 "영향 분석"플러그인.

이 그림

내 FRAMA-C의 현재 사용 가능한 플러그인을 보여줍니다

나는 또한 Frama-c web page 언급을하지만, 나에게 영향 분석 플러그인을 다운로드하거나 설치에 대한 모든 링크를 찾을 수 없습니다.

우분투 14.04에서 영향 분석을 어떻게 활성화하고 사용할 수 있습니까?

Answer 1

Impact 플러그인은 Nea-20140301 버전 이후로 이미 Frama-C와 함께 설치되어 있으며이를 사용하려면 특별한 작업을 수행 할 필요가 없습니다. 문장을 선택하고 활성화 할 수있는 적절한 상황에 맞는 메뉴를 찾으십시오. 당신이 언급 한 FRAMA-C 웹 페이지에서

은 (굵은 관련 부분에 강조 표시) :

영향 분석은 FRAMA-C 그래픽 사용자 인터페이스의 각 문에서 상황에 맞는 메뉴를 통해 사용할 수 있습니다 .

는

스크린 샷의 왼쪽 창, 이러한 플러그인 플러그인 패널의 목록 (파일 이름 및 전역 변수/함수, 상부)에 filetree를 포함하는 자체 GUI 패널을 등록했습니다. 모든 플러그인이 연관된 패널을 가지고있는 것은 아닙니다. 예를 들어 Impact는 컨텍스트 메뉴를 통해서만 사용할 수있는 플러그인입니다.

Frama-C 웹 사이트의 Impact 플러그인 페이지를 자세히 살펴보면 표시된 스크린 샷에는 스크린 샷에 GUI 부분이 포함되어 있지 않지만 대신 왼쪽 부분은 이미 Cil입니다. 코드 (스크린 샷 생략) :

이 스크린 샷에 표시된 팝업 메뉴를 얻으려면, 당신은 문를 가질뿐만 아니라 식을 강조 표시된 필요합니다. 스크린 샷에서 전체 p = T; 문이 강조 표시됩니다. 그렇지 않으면 컨텍스트 메뉴에 "영향 분석"항목이 표시되지 않습니다.

Frama-C GUI에서 명령문을 선택하는 가장 쉬운 방법은 을 클릭하고 세미콜론 인을 클릭하는 것입니다. 위의 스크린 샷과 같이 지정 문인 경우 등호를 클릭하여 문을 선택할 수도 있습니다. 그러나 p 또는 T을 직접 클릭하면 해당 변수에 해당하는 표현식 만 선택됩니다. Impact는 표현식이 아닌 명령문을 기반으로하므로이 경우 상황에 맞는 메뉴는 표시되지 않습니다.

그런데 Frama-C 설치에서 특정 플러그인을 사용할 수 있는지 확인하려면 frama-c -plugins을 실행하여 설치된 플러그인 목록을 가져 오거나 GUI (메뉴 분석/분석) : 플러그인 당 하나의 항목이 들어 있습니다.

편집 : VM을 함께 테스트 후, 나는 우분투 14.04 (트러스티)가 충격 플러그인을 가지고 않았다 아주 오래된 버전의 패키지 (2013) FRAMA-C 불소를 가지고 실현, 그러나 어떤 이유로 그것은 당시 데비안 꾸러미에 포함되지 않았습니다 (그래서 그것을 사용할 수 없습니다). Frama-C는 빠르게 진화하고 있습니다. 따라서 오래된 버전을 사용하면 몇 가지 문제가 발생합니다. OPAM을 통해 설치하는 것이 좋습니다.