goto-cc - 클라우드에서의 온라인

프로그램:

이름

cbmc - C/C++ 및 Java 프로그램용 경계 모델 검사기

개요

cbmc [--재산 속성 ID] 파일.c ...

cbmc [--표시 속성] 파일.c ...

cbmc [--모든 속성] 파일.c ...

goto-cc [-NS 포함 경로] [-씨] 파일.c [-또는 outfile.o]

고토 악기 인파일 아웃파일

가장 유용한 옵션만 여기에 나열됩니다. 나머지는 아래를 참조하십시오.

기술

cbmc 어설션이 위반될 수 있는 방법을 보여 주는 추적을 생성하거나 다음을 증명합니다.
어설션은 주어진 루프 반복 횟수 내에서 위반될 수 없습니다. CBMC는 읽을 수 있습니다
소스 코드 직접 또는 goto-cc에 의해 생성된 goto-binary. Java 프로그램은 다음과 같이 제공됩니다.
클래스 파일. 추가 옵션 없이 cbmc는 모든 속성을 확인합니다(자동으로
생성 또는 사용자 지정) 프로그램에서 찾을 수 있습니다. 속성 중 하나가 될 수 있는 경우
위반되면 반례가 인쇄되고 분석이 중단됩니다. 분석은
--property 옵션을 사용하여 특정 속성으로 제한됩니다. 검증 결과
--all-properties 옵션을 사용하여 모든 속성을 얻을 수 있습니다.

goto-cc 소스 코드를 읽고 goto-binary를 생성합니다. 명령줄 인터페이스는 다음과 같습니다.
의 것을 모방하도록 설계 GCC(1). 특히 goto-cc ~을 구별하다
gcc가 하는 것처럼 단계를 컴파일하고 연결합니다. cbmc goto-binary를 기대합니다.
연동이 완료되었습니다.

고토 악기 goto-binary를 읽고 주어진 프로그램 변환을 수행한 다음
결과 프로그램을 디스크에 goto-binary로 기록합니다.

일반적인 흐름은 (1) goto-cc를 사용하여 소스를 goto-binary로 변환한 다음 (2)
goto-instrument로 계측을 수행하고 마지막으로 (3) 다음을 사용하여 분석을 수행합니다.
cbmc.

옵션

FRONTEND 옵션 (cbmc 과 goto-cc)
-나는 길
포함 경로 설정(C/C++)

-D 매크로
전처리기 매크로 정의(C/C++)

--전처리
전처리 후 중지

--show-심볼-테이블
기호 테이블 표시

--show-goto-기능
goto 프로그램 표시

건축 옵션 (cbmc 과 goto-cc)
cbmc 기본적으로 시스템의 설정과 일치하는 아키텍처 설정을 사용합니다. cbmc is
즉, 아래 설정은 실행 중인 소프트웨어를 확인할 때만 필요합니다.
다른 아키텍처 또는 OS에서 실행되는 것을 의미합니다. goto-cc 대한 goto-binary를 생성합니다.
특정 아키텍처, 즉 goto-binary가 변경된 후에는 아키텍처를 변경할 수 없습니다.
생성.

--16, --32, --64
int의 너비 설정

--LP64, --ILP64, --LLP64, --ILP32, --LP32
int, long 및 포인터의 너비 설정

--리틀 엔디안
little-endian 워드-바이트 변환 허용

--빅 엔디안
빅 엔디안 워드 바이트 변환 허용

--부호 없는 문자
기본적으로 "char"를 부호 없는 것으로 만듭니다.

--arch 대상 아키텍처 설정

--os 대상 운영 체제 설정

--아치 없음
아키텍처를 설정하지 마십시오.

--라이브러리 없음
내장 추상 C 라이브러리 비활성화

--가장 가까운 값으로 반올림, --+inf로 반올림, ---inf로 반올림, --XNUMX으로 반올림
프로그램이 시작될 때 사용할 IEEE 부동 소수점 반올림 모드(기본값은 반올림
가장 가까운). 확인 중인 프로그램은 이 설정을 무시할 수 있습니다.
페셋 라운드(3).

프로그램 수단 옵션 (cbmc 과 고토 악기)
모두 cbmc 과 고토 악기 특정 공통 오류를 포착하는 어설션을 생성할 수 있습니다.
으로는 다음과 같습니다.

--경계 검사
배열 범위 확인 활성화

--div-by-zero-검사
XNUMX으로 나누기 확인 활성화

--포인터 검사
포인터 확인 활성화

--서명-오버플로-확인
부호 있는 정수 산술에 대한 산술 오버플로 및 언더플로 검사 활성화

--unsigned-오버플로-확인
부호 없는 정수 산술에 대한 산술 오버플로 및 언더플로 검사 활성화

--난-체크
NaN에 대한 부동 소수점 계산 확인

--어설션 없음
사용자 제공 어설션 무시

--가정 없음
사용자가 제공한 가정 무시

--오류 레이블 레이블
지정된 레이블에 도달할 수 없는지 확인하십시오.

프로그램 수단 옵션 (고토 악기 만 해당)
고토 악기 더 복잡하고 더 복잡한 프로그램 변환을 지원합니다.

--nondet-휘발성
휘발성 변수의 읽기를 비결정적으로 만듭니다.

--isr 함수
지정된 이름으로 인터럽트 서비스 루틴 계측

--mmio Instruments 메모리 매핑 I/O

--nondet-정적
정적 수명이 있는 변수는 비결정적으로 초기화됩니다.

--덤프-c
goto 바이너리 대신 ANSI-C 소스 코드를 출력합니다.

BMC 옵션 (CBMC)
--모든 속성
모든 속성의 상태 보고

--표시 속성
속성만 표시

--쇼 루프
프로그램에 루프 표시

--표지 주장
도달 가능한 어설션 확인

--함수 이름
주요 기능 이름 설정

--속성 ID
주어진 식별자를 가진 특정 속성만 확인

--프로그램 전용
프로그램 표현식만 표시

--깊이 번호
검색 깊이 제한

--풀기 번호
루프 nr 번 풀기

--L:B 설정 해제,...
경계 B로 루프 L 풀기(루프 ID를 가져오려면 --show-loops 사용)

--show-vcc
확인 조건 표시

--슬라이스 공식
속성과 관련 없는 할당 제거

--no-unwinding-어설션
해제 어설션을 생성하지 마십시오.

--예쁜 이름 없음
식별자를 단순화하지 마십시오

백엔드 옵션 (CBMC)
--디막스
외부 SAT 솔버에서 사용할 DIMACS 형식의 CNF 생성

--beautify-탐욕스러운
반례를 미화하라(욕심 휴리스틱)

--smt1 SMT1 구문의 하위 목표 출력(실험적)

--smt2 SMT2 구문의 하위 목표 출력(실험적)

--부울렉터
Boolector 사용(실험적)

--mathsat
MathSAT 사용(실험적)

--cvc CVC3 사용(실험적)

--yices
Yices 사용(실험적)

--z3 Z3 사용(실험적)

--정제
정제 절차 사용(실험적)

--outfile 파일 이름
주어진 파일로 수식 출력

--배열-uf-절대
배열을 해석되지 않은 함수로 바꾸지 마십시오.

--배열-uf-항상
항상 배열을 해석되지 않은 함수로 변환

환경

모든 도구는 임시 파일을 생성할 때 TMPDIR 환경 변수를 따르고
디렉토리. 또한 CBMC에서 사용하는 전처리기는 환경을 사용합니다.
헤더 파일을 찾기 위한 변수. GOTO-CC는 모든 환경 변수를 받아들이는 것을 목표로 합니다.
GCC가 합니다.

저작권

2001-2014, 다니엘 크로닝, 에드먼드 클라크

onworks.net 서비스를 사용하여 온라인으로 goto-cc를 사용하세요.