Frama C snapshot

Frama-C는 C로 작성된 소스 코드 분석 전용 플랫폼입니다.

참고 : 공식 Frama-C 저장소는 이제 Gitlab에 있습니다!

Frama-C는 공식 저장소를 자체 주최 Gitlab 인스턴스로 옮겼습니다.

공식 릴리스 (Frama-C 21부터 시작)는 더 이상 여기에서 업데이트되지 않습니다.

야간 스냅 샷은 Gitlab에서도 제공됩니다! 이제 https://git.frama-c.com/pub/frama-c/-/tree/master의 최신 개발 버전에 액세스 할 수 있습니다.

공식 Frama-C 문제 추적기는 이제 Gitlab에 있습니다 : https://git.frama-c.com/pub/frama-c/-/issues

GitHub 로그인을 사용하여 문제를 제출하고 요청을 가져올 수 있습니다 (프롬프트시 "GitHub로 로그인"을 선택하십시오).

거기서 만나요!

협업 플랫폼

Frama-C는 단일 협업 플랫폼에서 여러 분석 기술을 수집합니다. 단일 협업 플랫폼에서 핵심 기능 세트 (예 : C 프로그램의 정규화 된 AST)와 플러그인 이라는 분석기 세트를 제공하는 커널 로 구성됩니다. 플러그인은 플랫폼의 다른 플러그인으로 계산 된 결과를 구축 할 수 있습니다.

이 접근 방식 덕분에 Frama-C는 다음을 포함한 정교한 도구를 제공합니다.

• 런타임 오류 ( EVA )가없는 것을 목표로하는 추상 해석을 기반으로 한 분석기;
• 가장 약한 전제 조건 미적분학 ( WP )에 기초한 프로그램 증거 프레임 워크;
• 프로그램 슬라이서 ( 슬라이스 );
• 시간 (LTL) 특성 검증 도구 ( Aoraï );
• 런타임 검증 도구 ( e-ACSL );
• 코드 기반 탐색 및 종속성 분석을위한 몇 가지 도구 ( From , Impact , Metrics , Virtrence , Scope 등).

이 플러그인은 공통 언어를 공유하며 ACSL ( ANSI/ISO C 사양 언어 ) 속성을 통해 정보를 교환 할 수 있습니다. 플러그인은 API를 통해 협력 할 수도 있습니다.

설치

OPAM/FRAMA-C 설치에 대한 자세한 정보는 install.md를 참조하십시오.

Frama-C는 OCAML 패키지 관리자 인 OPAM을 통해 제공됩니다. 이것은 선호되는 설치 방법입니다. Opam v2.0 이상을 설치하십시오. 그런 다음 다음의 명령 시퀀스는 Frama-C와 GUI를 설치해야합니다.

 opam init
opam install depext
opam depext frama-c
opam install frama-c

Frama-C는 주로 Linux에서 개발되며 종종 MacOS (홈브류를 통해)로 테스트되었으며 때로는 Windows (Linux의 Windows 하위 시스템을 통해)에서 테스트됩니다.

용법

Frama-C는 명령 줄에서 또는 그래픽 인터페이스를 통해 실행할 수 있습니다.

간단한 사용

간단한 파일에 권장되는 사용법은 다음 줄 중 하나입니다.

 frama-c file.c -<plugin> [options]
frama-c-gui file.c

여기서 -<plugin> 은 여러 Frama -C 플러그인, 예를 들어 -eva 또는 -wp , 또는 -metrics 등입니다. 플러그인은 GUI에서 직접 실행할 수 있습니다.

모든 플러그인을 나열하려면 실행하십시오.

 frama-c -plugins

각 플러그인에는 여러 옵션을 설명하는 Help Command ( -<plugin>-help 또는 -<plugin>-h )가 있습니다.

마지막으로 Frama-C의 커널 자체의 동작을 지배하는 옵션 목록은

 frama-c -kernel-help

복잡한 시나리오

보다 복잡한 사용 시나리오 (여러 파일 및 디렉토리, 여러 전처리 지시문)를 위해 Frama-C의 사용을 두 부분으로 나누는 것이 좋습니다.

1. 입력 파일을 구문 분석하고 결과를 파일에 저장합니다.
2. 구문 분석 결과를로드 한 다음 분석 또는 GUI를 실행합니다.

구문 분석은 일반적으로 C 사전 프로세서에 추가 인수를 제공하는 것이 포함되므로 -cpp-extra-args 옵션은 다음 예에서와 같이 종종 유용합니다.

 frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

그런 다음 결과를 추가 분석 또는 GUI를 통한 검사를 위해 FRAMA-C에로드합니다.

 frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

추가 참조

• 사용자 및 개발자 설명서, Frama-C 아카이브 및 플러그인 매뉴얼에 대한 링크는 다음과 같습니다.
  http://frama-c.com/download.html

• StackoverFlow에는 Frama-C Community의 여러 회원이 모니터링하는 frama-c 태그와 몇 가지 질문이 있습니다.

• Frama-C-Discuss 메일 링리스트는 공지 및 일반 토론에 사용됩니다.

• 공식 버그 추적 시스템은 버그 보고서에 사용될 수 있습니다.

• Frama-C Wiki에는 유용한 정보가 있지만 전적으로 최신 정보는 아닙니다.

• Frama-C 블로그에는 FRAMA-C의 새로운 개발에 대한 몇 가지 게시물과 C 언어, 정의되지 않은 행동, 부동 소수점 계산 등에 대한 일반적인 토론이 있습니다.

• Github 스냅 샷 저장소에는 Clame의 .tar.gz 아카이브가 포함되어 있으며 클로닝 될 준비가되었습니다. 또한 문제를보고하고 풀 요청을 제출하는 데 사용될 수 있습니다.