frama-c-gui - 클라우드에서의 온라인

프로그램:

이름

frame-c[.byte] - C 프로그램용 정적 분석기

frama-c-gui[.byte] - frama-c의 그래픽 인터페이스

개요

프레임-C [ 옵션 ] 파일

기술

프레임-C C로 작성된 소스 코드 분석 전용 도구 모음입니다.
단일 협업 프레임워크에서 여러 정적 분석 기술을 수집합니다. 이것
프레임워크는 추가 플러그인에 의해 확장될 수 있습니다. $FRAMAC_PLUGIN 디렉토리.
명령

프레임-c -도움말

현재 설치된 플러그인의 전체 목록을 제공합니다.

프레임-c-gui 의 그래픽 사용자 인터페이스입니다. 프레임-C. 와 같은 옵션을 제공합니다.
명령줄 버전.

프레임 c.byte 과 프레임-c-gui.byte 명령줄의 ocaml 바이트코드 버전이며
그래픽 사용자 인터페이스.

기본적으로 Frama-C는 .c 전처리가 필요한 C 파일로 파일 및 .i 파일
C 파일은 이미 사전 처리되었습니다. 일부 플러그인은 인식 목록을 확장할 수 있습니다.
파일. 전처리는 다음을 통해 사용자 지정할 수 있습니다. -cpp 명령 과 -cpp-추가-인수
옵션을 제공합니다.

옵션

통사론

추가 매개변수를 사용하는 옵션은 다음 형식으로도 작성할 수 있습니다.

-선택권=내 돈

이 옵션은 다음과 같은 경우에 필수입니다. 내 돈 대시('-')로 시작

매개변수를 사용하지 않는 대부분의 옵션에는 해당하는 매개변수가 있습니다.

-아니-선택권

반대 효과가 있는 옵션입니다.

도움말 옵션

-도움 짧은 사용 안내와 설치된 플러그인 목록을 제공합니다.

-커널 도움말
Frama-C의 커널이 인식하는 옵션 목록을 출력합니다.

-말 수가 많은 n
상세 수준을 설정합니다(기본값은 1). 0으로 설정하면 진행률이 낮아집니다.
메시지. 이 수준은 당에서 설정할 수도 있습니다. 플러그인 기본, 옵션 포함 -플러그인-
말 수가 많은 n. 커널의 상세 수준은 옵션으로 제어할 수 있습니다.
-커널 상세 정보 n.

-디버그 n
디버깅 수준을 설정합니다(기본값은 0, 디버깅 메시지가 없음을 의미). 이 옵션
플러그인(및 커널)별 전문화는 다음과 동일합니다. -말 수가 많은.

-조용한 세부 정보 표시 및 디버깅 수준을 0으로 설정합니다.

옵션 제어 Frama-C의 커널

-절대 유효 범위
범위의 모든 숫자 주소를 고려합니다. 최소 최대 유효합니다. 경계는
ocaml 정수 상수로 구문 분석됩니다. 기본적으로 모든 숫자 주소는
무효로 간주됩니다.

-추가 경로 p1[,p2[...,pn]]
디렉토리를 추가합니다 을 통하여 플러그인이 있는 디렉토리 목록에
검색된

[-no]-허용-중복
테스트 및 루프의 정규화 중에 작은 블록의 복제를 허용합니다.
그렇지 않으면 정규화는 레이블과 gotos를 사용합니다. 더 큰 블록과 비
사소한 제어 흐름은 절대 복제되지 않습니다. 기본값은 예입니다.

[-no]-주석
ACSL 주석을 읽습니다. 이것이 기본값입니다. 주석은 사전 처리되지 않습니다.
기본. 사용 -pp-annot 그에 대한.

-big-int-hex 최대
보다 큰 정수 최대 XNUMX진수로 표시됩니다(기본적으로 모든 정수는
XNUMX진수로 표시)

-검사 내부 AST에 대한 무결성 검사를 수행합니다(개발자 전용).

[-no]-collapse-call-cast
함수가 반환한 값과 lvalue 간의 암시적 캐스트를 허용합니다.
할당. 그렇지 않으면 임시 변수가 사용되고 캐스트가 명시적으로 이루어집니다.
기본값은 예입니다.

[-아니요]-constfold
분석 전에 코드의 구문상 상수 표현식을 모두 접습니다. 기본값
아니오.

[-no]-계속-annot-오류
주석을 분석할 때 기본 동작( -아니 이 옵션의 버전)
유형 검사 오류가 발생하면 소스 파일을 거부하는 것입니다.
C 코드 내의 유형 검사 오류. 이 옵션을 켜면 유형 검사기가
경고만 출력하고 주석을 버리지만 유형 검사는 계속됩니다.
(하지만 C 코드의 오류는 여전히 치명적입니다.)

-cpp 명령 cmd를
사용 cmd를 C 파일을 사전 처리하는 명령으로. 기본값은 CPP 환경
변수 또는

gcc -C -E -I.

설정되지 않은 경우. ACSL 주석을 보존하기 위해 전처리기는 다음을 유지해야 합니다.
댓글( -C gcc 옵션). %1 과 %2 에서 사용될 수 있습니다 cmd를 나타내다
원본 소스 파일과 사전 처리된 파일 각각

-cpp-추가-인수 인수
전처리기에 추가 인수를 제공합니다. 이 경우에만 유용합니다.
-전처리 주석 설정됩니다. 전처리 주석은 두 개의 개별 전처리에서 수행됩니다.
처리 단계. 첫 번째는 매크로를 유지하는 C 코드의 일반 패스입니다.
정의. 그런 다음 주석이 생성되는 두 번째 패스에서 사용됩니다.
전처리. 인수 첫 번째 패스에만 사용되므로 인수는
두 번 사용하면 안 됩니다(예: 추가 include 지시문 또는 매크로
정의) 따라서 대신 거기에 가야합니다 -cpp 명령.

[-아니요]-dynlink
설정하면 검색 경로에서 찾은 모든 동적 플러그인을 로드합니다(참조: -인쇄 플러그인-
통로 기본 검색 경로에 대한 자세한 내용은 참조). 그렇지 않으면 플러그인만
에 의해 요청 -로드 모듈 로드됩니다. 기본 동작은 켜져 있습니다.

-열거형 재현
열거 유형의 표현이 결정되는 방식을 선택합니다. 프레임-C
-열거형 도움 사용 가능한 옵션 목록을 제공합니다. 기본값은 gcc 열거형

-부동수 n
부동 소수점 숫자를 출력할 때 표시 n 숫자. 기본값은 12입니다.

-float-flush-to-XNUMX
부동 소수점 연산이 XNUMX으로 플러시

-float-hex
플로트를 XNUMX진수로 표시

-플로트 노멀
표준 Ocaml 루틴으로 플로트 표시

-float 상대
부동 간격을 [로 표시 하한++폭 ]

[-no]-force-rl-arg-eval
함수 호출의 인수에 대해 오른쪽에서 왼쪽으로 평가 순서를 지정합니다. 그렇지 않으면
평가 순서는 C 표준에서와 같이 지정되지 않은 상태로 유지됩니다. 기본값은 아니요입니다.

-저널 비활성화
현재 세션의 저널을 출력하지 마십시오. 보다 -저널 활성화.

-저널 활성화
기본적으로 켜져 있는 동안 수행된 모든 작업의 ​​저널을 덤프합니다.
재생할 수 있는 ocaml 스크립트 형태의 Frama-C 세션 -짐-
스크립트. 스크립트의 이름은 다음과 같이 설정할 수 있습니다. -저널 이름 옵션을 선택합니다.

-저널 이름 name
저널 파일의 이름을 설정합니다( .ml 확대). 기본값은
frame_c_journal.

-초기화-패딩-로컬
로컬의 암시적 초기화는 패딩 비트를 0으로 설정합니다. false인 경우 패딩 비트
초기화되지 않은 상태로 남습니다(기본값은 yes).

[-no]-유지-주석
소스 코드를 예쁘게 인쇄할 때 주석을 보존하려고 시도합니다(기본값은 no).

[-no]-유지-스위치
인셀덤 공식 판매점인 -단순화-cfg 가 설정되면 switch 문을 유지합니다. 기본값은 아니요입니다.

-사용되지 않은 지정된 기능 유지
만나다 -사용되지 않은 지정된 기능 제거

[-no]-lib 항목
프로그램 실행 중에 진입점이 호출됨을 나타냅니다. 이것은 다음을 의미합니다.
특히 전역 변수는 초기 값을 가질 수 없다고 가정할 수 있습니다.
디폴트는 -lib 항목 없음: 진입점은 의 시작점이기도 합니다.
프로그램과 전역은 초기 값을 갖습니다.

-하중 파일
에 포함된 (이전에 저장된) 상태를 로드합니다. 파일.

-로드 모듈 m1[,m2[...,mn]]
ocaml 모듈 로드 을 통하여 . 이러한 모듈은 .cmxs파일
Frama-c의 네이티브 코드 버전 및 .cmoor.cma바이트코드 버전용 파일(참조
자세한 내용은 Ocaml 설명서의 Dynlink 섹션 참조). 모든 모듈은
플러그인 검색 경로에 있는 플러그인은 자동으로 로드됩니다.

-로드 스크립트 s1[,s2,[...,sn]]
ocaml 스크립트를 로드합니다. 을 통하여 . 스크립트는 .ml파일. 그들
Ocaml 표준 라이브러리와 Frama-C의 API에만 의존하여 컴파일 가능해야 합니다. 만약에
일부 사용자 지정 컴파일 단계가 필요합니다. Frama-C 외부에서 컴파일하고 사용
-로드 모듈 대신.

-machdep 기계
사용 기계 현재 기계 종속 구성(다양한
정수 유형, endiandness, ...). 현재 지원되는 머신 목록은 다음과 같습니다.
통해 사용할 수 -machdep 도움 옵션. 기본값은 x86_32

-본관 f
설정 f 분석의 진입점으로. 기본값은 '메인'입니다. 기본적으로
분석 중인 프로그램의 시작점으로 간주됩니다. 사용 -lib 항목 if f
실행 중간에 호출되어야 합니다.

- 난독화
코드의 난독화된 버전을 인쇄합니다(여기서 원래 식별자는 교체됨).
무의미한 것으로) 종료합니다. 오리지날과 뉴의 대응표
기호는 결과의 시작 부분에 유지됩니다.

-ocode 파일
예쁘게 인쇄된 코드를 파일 표준 출력 대신.

[-no]-원본 이름
정규화 단계에서 일부 변수는 다른 경우 이름이 변경될 수 있습니다.
동일한 이름을 가진 변수가 공존할 수 있습니다(예: 전역 변수 및 형식
매개변수). 이 옵션이 켜져 있으면 이 문제가 발생할 때마다 메시지가 인쇄됩니다.
기본값은 아니요입니다.

[-아니요]-경고-서명-다운캐스트
서명된 다운캐스트가 대상 범위를 초과할 수 있는 경우 경보 생성(기본값은
아니).

[-아니요]-경고-서명-오버플로
오버플로되는 서명된 작업에 대한 경보를 생성합니다(기본값은 yes).

[-아니요]-경고-서명되지 않은-다운캐스트
서명되지 않은 다운캐스트가 대상 범위를 초과할 수 있는 경우 경보 생성(기본값)
아니오).

[-아니요]-경고-부호 없음-오버플로
오버플로되는 서명되지 않은 작업에 대한 경보를 생성합니다(기본값은 no).

[-아니요]-pp-annot
전처리 주석. 이것은 현재 gcc(또는 GNU)를 사용할 때만 가능합니다.
cpp) 전처리기. 기본값은 주석을 전처리하지 않는 것입니다.

[-no]-인쇄
CIL에 의해 정규화된 대로 소스 코드를 예쁘게 인쇄합니다(기본값은 no).

-인쇄 라이브러리 경로
Frama-C 커널 라이브러리가 설치된 디렉토리 출력

-인쇄 경로
별칭 -인쇄 공유 경로

-인쇄 플러그인 경로
Frama-C가 플러그인을 검색하는 디렉토리를 출력합니다(
FRAMAC_PLUGIN 변수 및 -추가 경로 선택권)

-인쇄 공유 경로
Frama-C가 데이터를 저장하는 디렉토리를 출력합니다(
FRAMAC_SHARE 변하기 쉬운)

-사용되지 않은 지정된 기능 제거
ACSL 사양이 있지만 사용되지 않는 함수 프로토타입을 유지합니다.
암호. 이것이 기본값입니다. 속성이 있는 함수 FRAMAC_BUILTIN 항상
유지 된.

-안전 배열
다차원 배열 또는 structs 내부의 필드인 배열의 경우 다음을 가정합니다.
모든 액세스는 인바운드여야 합니다(기본적으로 설정됨). 반대 옵션은 -위험한-
배열

-저장 파일
Frama-C의 상태를 다음으로 저장합니다. 파일 분석이 이루어진 후.

[-no]-단순화-cfg
분석 전에 break, continue 및 switch 문을 제거합니다. 기본값은 아니요입니다.

-그 다음에 분석을 구성할 수 있습니다. Frama-C의 첫 번째 실행은 옵션과 함께 발생합니다.
전에 -그 다음에 다음 옵션으로 두 번째 실행이 수행됩니다. -그 다음에 를 시청하여 이에 대해 더 많은 정보를 얻을 수 있습니다.
첫 실행부터 현재 프로젝트.

-그때 홍보
유사하게 -그 다음에 두 번째 실행이 프로젝트에서 수행되는 것을 제외하고 홍보 그러한 것이 없다면
프로젝트가 존재하면 Frama-C가 오류와 함께 종료됩니다.

-시각 파일
주어진 사용자 시간과 날짜를 추가합니다. 파일 Frama-C가 종료될 때.

-타입 검사
소스 파일의 유형 검사를 강제합니다. 이 옵션은 더 이상
분석이 요청된 경우(유형 검사가 분석 전에 암시적으로 발생하기 때문입니다.
론칭).

-u레벨 n
문법적으로 루프 풀기 n 분석 전 시간. 비용이 많이 들 수 있습니다.
일부 플러그인(예: 가치 분석)은 보다 효율적인 수행 방법을 제공합니다.
똑같은 것. 자세한 내용은 해당 설명서를 참조하십시오. 이것은 또한 할 수 있습니다
를 통해 루프별로 활성화됩니다. 고리 프라그마 풀다 지령. ㅏ
에 대한 음수 값 n 이러한 pragma를 금지합니다.

[-no]-유니코드
utf8 문자로 ACSL 수식을 출력합니다. 이것이 기본값입니다. 주어진 때
-유니코드 없음 옵션에서 Frama-C는 대신 ASCII 버전을 사용합니다. ACSL 설명서 참조
대응을 위해.

-unsafe-배열
참조 -안전 배열

[-no]-지정되지 않은 액세스
지정되지 않은 순서로 발생하는 읽기/쓰기 액세스를 확인합니다(C
표준의 시퀀스 포인트 개념)은 별도의 위치에서 수행됩니다. 와 함께
-지정되지 않은 액세스 없음, 항상 그렇다고 가정합니다(기본값).

-번역
Frama-C의 버전 문자열 출력

-경고-소수-부동
부동 소수점 상수를 정확히 표현할 수 없을 때(예: 0.1) 경고합니다.
중 하나가 될 수 있습니다 없음, 일단및 모든

[-아니요]-선언되지 않은 수신자 경고
함수가 선언되기 전에 호출되면 경고합니다(기본값으로 설정됨).
프라 마 -C

플러그인 구체적인 옵션

각각 플러그인, 명령

프레임-c-플러그인-도움

플러그인에 특정한 옵션 목록을 제공합니다.

EXIT 지위

0 성공적인 실행

1 잘못된 사용자 입력

2 사용자 중단(kill 또는 동등)

3 구현되지 않은 기능

4 5 6 내부 오류

125 알수없는 오류

2보다 큰 종료 상태는 버그(또는 경우에 대한 기능 요청)로 간주될 수 있습니다.
종료 상태 3) 및 Frama-C의 BTS(아래 참조)에서 보고될 수 있습니다.

환경 변수

Frama-C가 파일을 찾는 위치를 제어할 수 있습니다.
다음 변수.

FRAMAC_LIB
커널의 컴파일된 인터페이스가 설치된 디렉토리

FRAMAC_PLUGIN
Frama-C가 표준 플러그인을 찾을 수 있는 디렉토리. 플러그인을 원하시면
여러 곳에서 사용 -추가 경로 대신.

FRAMAC_SHARE
Frama-C 데이터가 설치된 디렉토리.

onworks.net 서비스를 사용하여 온라인에서 frama-c-gui 사용