goto-cc - Trực tuyến trên đám mây

CHƯƠNG TRÌNH:

TÊN

cbmc - Trình kiểm tra mô hình có giới hạn cho các chương trình C / C ++ và Java

SYNOPSIS

cbmc [--bất động sản id thuộc tính] tập tin.c hữu ích. Cảm ơn !

cbmc [--show-thuộc tính] tập tin.c hữu ích. Cảm ơn !

cbmc [- tất cả-thuộc tính] tập tin.c hữu ích. Cảm ơn !

goto-cc [-TÔI bao gồm đường dẫn] [-NS] tập tin.c [-hoặc là outfile.o]

goto-cụ trong tập tin ô uế

Chỉ những tùy chọn hữu ích nhất được liệt kê ở đây; xem phần còn lại bên dưới.

MÔ TẢ

cbmc tạo ra các dấu vết chứng minh cách một khẳng định có thể bị vi phạm hoặc chứng minh rằng
khẳng định không thể bị vi phạm trong một số lần lặp vòng lặp nhất định. CBMC có thể đọc
mã nguồn trực tiếp hoặc goto-binary được tạo bởi goto-cc. Các chương trình Java được cung cấp dưới dạng
các tệp lớp. Nếu không có bất kỳ tùy chọn nào khác, cbmc sẽ kiểm tra tất cả các thuộc tính (tự động
được tạo hoặc do người dùng chỉ định) được tìm thấy trong chương trình. Nếu bất kỳ thuộc tính nào có thể
vi phạm, một mẫu đối chiếu được in ra và quá trình phân tích bị hủy bỏ. Phân tích có thể
bị hạn chế đối với một thuộc tính cụ thể với tùy chọn --property. Kết quả xác minh
cho tất cả các thuộc tính có thể được lấy bằng tùy chọn - tất cả các thuộc tính.

goto-cc đọc mã nguồn và tạo goto-binary. Giao diện dòng lệnh của nó là
được thiết kế để bắt chước gcc(1). Đặc biệt lưu ý rằng goto-cc phân biệt giữa
biên dịch và liên kết các giai đoạn, giống như gcc. cbmc mong đợi một goto-binary cho
liên kết đã được hoàn thành.

goto-cụ đọc một goto-binary, thực hiện một chuyển đổi chương trình nhất định, và sau đó
ghi chương trình kết quả dưới dạng goto-binary trên đĩa.

Quy trình thông thường là (1) dịch nguồn thành tệp nhị phân goto bằng cách sử dụng goto-cc, sau đó (2)
thực hiện thiết bị đo đạc với goto-tools và cuối cùng (3) thực hiện phân tích với
cbmc.

LỰA CHỌN

Lối vào LỰA CHỌN (cbmc và goto-cc)
Tôi con đường
Đặt đường dẫn bao gồm (C / C ++)

-D vĩ mô
Xác định macro bộ xử lý trước (C / C ++)

- quy trình
Dừng sau khi xử lý trước

--show-Symbol-table
Hiển thị bảng ký hiệu

--show-goto-chức năng
Hiển thị chương trình goto

KIẾN TRÚC LỰA CHỌN (cbmc và goto-cc)
cbmc theo mặc định sử dụng cài đặt kiến ​​trúc phù hợp với cài đặt của máy cbmc is
được thực thi trên, tức là, các cài đặt bên dưới chỉ cần thiết khi xác minh phần mềm
có nghĩa là để chạy trên một kiến ​​trúc hoặc hệ điều hành khác. goto-cc tạo goto-binary cho một
kiến trúc cụ thể, tức là, không thể thay đổi kiến ​​trúc sau khi goto-binary là
được tạo ra.

--16, --32, --64
Đặt chiều rộng của int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Đặt chiều rộng của int, long và con trỏ

--Little-endian
Cho phép chuyển đổi byte từ ít cuối cùng

--big-endian
Cho phép chuyển đổi byte từ-byte lớn

--unsigned-char
Đặt "char" không có dấu theo mặc định

--arch Đặt kiến ​​trúc mục tiêu

--os Đặt hệ điều hành mục tiêu

- không có vòm
Không thiết lập một kiến ​​trúc

- không có thư viện
Tắt thư viện trừu tượng C tích hợp sẵn

--round-to-near, --round-to-plus-inf, --round-to-less-inf, --round-to-zero
Chế độ làm tròn dấu chấm động IEEE để sử dụng khi chương trình bắt đầu (mặc định là làm tròn
gần nhất). Chương trình đang được xác minh có thể ghi đè cài đặt này, ví dụ: với
lễ hội(3).

CHƯƠNG TRÌNH THIẾT BỊ ĐO ĐẠC LỰA CHỌN (cbmc và goto-cụ)
Cả hai cbmc và goto-cụ có thể tạo ra các xác nhận bắt được các lỗi phổ biến cụ thể,
như được liệt kê dưới đây.

--bounds-kiểm tra
Bật kiểm tra giới hạn mảng

--div-by-zero-kiểm tra
Bật phép chia cho số không kiểm tra

- kiểm tra điểm
Bật kiểm tra con trỏ

- đã ký-tràn-kiểm tra
Bật kiểm tra thừa và thiếu số học cho số học số nguyên có dấu

--unsigned-tràn-kiểm tra
Bật kiểm tra thừa và thiếu số học cho số học số nguyên không dấu

--nan-kiểm tra
Kiểm tra tính toán dấu phẩy động cho NaN

--không xác nhận
Bỏ qua xác nhận do người dùng cung cấp

- không có giả định
Bỏ qua các giả định do người dùng cung cấp

- nhãn -error-label
Kiểm tra để đảm bảo rằng nhãn đã cho là không thể truy cập được

CHƯƠNG TRÌNH THIẾT BỊ ĐO ĐẠC LỰA CHỌN (goto-cụ chỉ)
goto-cụ hỗ trợ các phép biến đổi chương trình xa hơn, phức tạp hơn.

--nondet-dễ bay hơi
Làm cho các lần đọc từ các biến biến động không xác định

--isr chức năng
Công cụ một quy trình dịch vụ ngắt với tên đã cho

--mmio Instruments I / O được ánh xạ bộ nhớ

--nondet-tĩnh
Các biến có thời gian tồn tại tĩnh được khởi tạo không xác định

--dump-c
Đầu ra mã nguồn ANSI-C thay vì mã nhị phân goto.

BMC LỰA CHỌN (cbmc)
- tất cả các thuộc tính
Báo cáo trạng thái của tất cả các thuộc tính

--show-property
Chỉ hiển thị thuộc tính

--show-loop
Hiển thị các vòng lặp trong chương trình

--cover-khẳng định
Kiểm tra xác nhận nào có thể truy cập được

--Tên chức năng
Đặt tên chức năng chính

- id tài khoản
Chỉ kiểm tra thuộc tính cụ thể với số nhận dạng đã cho

--chỉ chương trình
Chỉ hiển thị biểu thức chương trình

--độ sâu nr
Giới hạn độ sâu tìm kiếm

--thư giãn nhé
Mở vòng lặp nr lần

--unwindset L: B, ...
Giải phóng vòng lặp L với giới hạn B (sử dụng --show-loops để lấy ID vòng lặp)

--show-vcc
Hiển thị các điều kiện xác minh

--slice-Formula
Xóa các nhiệm vụ không liên quan đến thuộc tính

--không-unwinding-khẳng định
Không tạo ra các xác nhận đang gỡ bỏ

- không có tên đẹp
Không đơn giản hóa số nhận dạng

QUAY LẠI LỰA CHỌN (cbmc)
--dimac
Tạo CNF ở định dạng DIMACS để người giải SAT bên ngoài sử dụng

- đẹp đẽ-tham lam
Làm đẹp cho mẫu đối chiếu (tham lam heuristic)

--smt1 Các mục tiêu con đầu ra theo cú pháp SMT1 (thử nghiệm)

--smt2 Các mục tiêu con đầu ra theo cú pháp SMT2 (thử nghiệm)

- máy thu tiền
Sử dụng Boolector (thử nghiệm)

--mathsat
Sử dụng MathSAT (thử nghiệm)

--cvc Sử dụng CVC3 (thử nghiệm)

--yice
Sử dụng Yices (thử nghiệm)

--z3 Sử dụng Z3 (thử nghiệm)

--lọc
Sử dụng quy trình sàng lọc (thử nghiệm)

--outfile tên tệp
Xuất công thức cho tệp đã cho

--arrays-uf-không bao giờ
Không bao giờ biến mảng thành các hàm không được thông dịch

--arrays-uf-luôn
Luôn biến mảng thành các hàm không được thông dịch

MÔI TRƯỜNG

Tất cả các công cụ đều tôn trọng biến môi trường TMPDIR khi tạo các tệp tạm thời và
các thư mục. Ngoài ra, lưu ý rằng bộ xử lý trước được sử dụng bởi CBMC sẽ sử dụng môi trường
các biến để định vị tệp tiêu đề. GOTO-CC nhằm mục đích chấp nhận tất cả các biến môi trường
GCC thì có.

BẢN QUYỀN

2001-2014, Daniel Kroening, Edmund Clarke

Sử dụng goto-cc trực tuyến bằng các dịch vụ onworks.net