frama-c-gui - Trực tuyến trên đám mây

CHƯƠNG TRÌNH:

TÊN

frama-c [.byte] - một bộ phân tích tĩnh cho các chương trình C

frama-c-gui [.byte] - giao diện đồ họa của frama-c

SYNOPSIS

frama-c [ lựa chọn ] các tập tin

MÔ TẢ

frama-c là một bộ công cụ dành riêng cho việc phân tích mã nguồn được viết bằng C. It
tập hợp một số kỹ thuật phân tích tĩnh trong một khuôn khổ hợp tác duy nhất. Cái này
khuôn khổ có thể được mở rộng bằng các plugin bổ sung được đặt trong $ FRAMAC_PLUGIN thư mục.
Lệnh

frama-c -trợ giúp

sẽ cung cấp danh sách đầy đủ các plugin hiện đã được cài đặt.

frama-c-gui là giao diện người dùng đồ họa của frama-c. Nó có các tùy chọn tương tự như
phiên bản dòng lệnh.

frama-c.byte và frama-c-gui.byte là các phiên bản ocaml bytecode của dòng lệnh và
giao diện người dùng đồ họa tương ứng.

Theo mặc định, Frama-C nhận dạng .c tệp dưới dạng tệp C cần xử lý trước và .i các tập tin như
Các tệp C đã được xử lý trước. Một số plugin có thể mở rộng danh sách các
các tập tin. Quá trình tiền xử lý có thể được tùy chỉnh thông qua -cpp-lệnh và -cpp-thêm-args
tùy chọn.

LỰA CHỌN

cú pháp

Tùy chọn lấy một tham số bổ sung cũng có thể được viết dưới biểu mẫu

-tùy chọn=tiền của tôi

Tùy chọn này là bắt buộc khi tiền của tôi bắt đầu bằng dấu gạch ngang ('-')

Hầu hết các tùy chọn không có tham số đều có

-Không-Lựa chọn

tùy chọn có tác dụng ngược lại.

Trợ giúp lựa chọn

-Cứu giúp đưa ra một thông báo sử dụng ngắn và danh sách các plugin đã cài đặt.

-kernel-trợ giúp
in danh sách các tùy chọn được nhân của Frama-C công nhận

-bèo thuyền n
Đặt mức độ chi tiết (mặc định là 1). Đặt nó thành 0 sẽ xuất ra ít tiến trình hơn
tin nhắn. Mức độ này cũng có thể được đặt trên mỗi Plugin cơ sở, với tùy chọn -Plugin-
dài dòng n. Mức độ chi tiết của hạt nhân có thể được kiểm soát bằng tùy chọn
-kernel-dài dòng n.

-gỡ lỗi n
Đặt mức gỡ lỗi (mặc định là 0, nghĩa là không có thông báo gỡ lỗi). Tùy chọn này
có cùng các chuyên môn cho mỗi plugin (và hạt nhân) như -bèo thuyền.

-Yên lặng Đặt độ chi tiết và mức độ gỡ lỗi thành 0.

Các lựa chọn kiểm soát Frama-C's hạt nhân

-absolute-valid-phạm vi
coi rằng tất cả các địa chỉ số trong phạm vi nhỏ nhất lớn nhất có giá trị. Giới hạn là
được phân tích cú pháp dưới dạng hằng số nguyên ocaml. Theo mặc định, tất cả các địa chỉ số là
được coi là không hợp lệ.

-add-path p1 [, p2 [..., pn]]
thêm thư mục thông qua vào danh sách các thư mục chứa các plugin
đã tìm kiếm

[-no] -cho phép-sao chép
cho phép nhân bản các khối nhỏ trong quá trình chuẩn hóa các bài kiểm tra và vòng lặp.
Nếu không, quá trình chuẩn hóa sử dụng nhãn và gotos. Các khối lớn hơn và các khối không
luồng điều khiển tầm thường không bao giờ bị trùng lặp. Mặc định là có.

[-no] -annot
đọc chú thích ACSL. Đây là mặc định. Chú thích không được xử lý trước bởi
vỡ nợ. Sử dụng -pp-chú thích cho điều đó.

-big-ints-hex tối đa
số nguyên lớn hơn tối đa được hiển thị ở dạng thập lục phân (theo mặc định, tất cả các số nguyên là
hiển thị dưới dạng số thập phân)

-kiểm tra thực hiện kiểm tra tính toàn vẹn trên AST nội bộ (chỉ dành cho nhà phát triển).

[-no] -collapse-call-cast
cho phép ép kiểu ngầm giữa giá trị được trả về bởi một hàm và giá trị của nó
phân công. Nếu không, một biến tạm thời được sử dụng và việc ép kiểu được thực hiện rõ ràng.
Mặc định là có.

[-no] -constfold
gấp tất cả các biểu thức hằng số cú pháp trong mã trước khi phân tích. Mặc định
đến không.

[-no] -continue-annot-error
Khi phân tích một chú thích, hành vi mặc định ( -Không phiên bản của tùy chọn này)
khi lỗi đánh máy xảy ra là từ chối tệp nguồn như trường hợp của
lỗi đánh máy trong mã C. Khi bật tùy chọn này, người đánh máy sẽ
chỉ xuất ra cảnh báo và loại bỏ chú thích nhưng việc đánh máy sẽ tiếp tục
(Mặc dù vậy, lỗi trong mã C vẫn rất nghiêm trọng).

-cpp-lệnh cmd
Sử dụng cmd như lệnh để xử lý trước các tệp C. Mặc định là CPP môi trường
biến hoặc thành

gcc -C -E-Tôi.

nếu nó không được thiết lập. Để duy trì các chú thích ACSL, bộ tiền xử lý phải giữ
ý kiến ​​(sự -C tùy chọn cho gcc). %1 và %2 có thể được sử dụng trong cmd để biểu thị
tệp nguồn gốc và tệp được xử lý trước tương ứng

-cpp-thêm-args args.
Cung cấp các đối số bổ sung cho bộ xử lý trước. Điều này chỉ hữu ích khi
-tiền xử lý-chú thích được thiết lập. Xử lý trước chú thích được thực hiện trong hai phần trước riêng biệt
các công đoạn xử lý. Cái đầu tiên là một đường chuyền bình thường trên mã C giữ lại macro
định nghĩa. Sau đó, chúng được sử dụng trong lần vượt qua thứ hai trong đó các chú thích
được xử lý trước. args. chỉ được sử dụng cho lần vượt qua đầu tiên, do đó các đối số
không nên được sử dụng hai lần (chẳng hạn như chỉ thị bao gồm bổ sung hoặc macro
định nghĩa) do đó phải đến đó thay vì -cpp-lệnh.

[-no] -dynlink
Khi bật, hãy tải tất cả các plugin động được tìm thấy trong đường dẫn tìm kiếm (xem -print-plugin-
con đường để biết thêm thông tin về đường dẫn tìm kiếm mặc định). Nếu không, chỉ có các plugin
được yêu cầu bởi -load-mô-đun sẽ được tải. Hành vi mặc định đang bật.

-enum đại diện
Chọn cách xác định đại diện của các kiểu liệt kê. frama-c
-enum giúp đỡ đưa ra danh sách các tùy chọn có sẵn. Mặc định là gcc-enum

-float-chữ số n
Khi xuất số dấu phẩy động, hiển thị n các chữ số. Mặc định là 12.

-float-flush-to-zero
Các hoạt động dấu chấm động chuyển về XNUMX

-float-hex
hiển thị nổi dưới dạng thập lục phân

-float-bình thường
màn hình nổi với quy trình Ocaml tiêu chuẩn

-float-họ hàng
hiển thị khoảng thời gian float dưới dạng [ chặn dưới++chiều rộng ]

[-no] -force-rl-arg-eval
buộc thứ tự đánh giá từ phải sang trái cho các đối số của lời gọi hàm. Nếu không thì
thứ tự đánh giá không được xác định, như trong tiêu chuẩn C. Mặc định là không.

-journal-vô hiệu hóa
Không xuất nhật ký của phiên hiện tại. Nhìn thấy -journal-kích hoạt.

-journal-kích hoạt
Theo mặc định, ghi nhật ký về tất cả các hành động được thực hiện trong thời gian hiện tại
Phiên Frama-C ở dạng tập lệnh ocaml có thể được phát lại với -trọng tải-
kịch bản. Tên của tập lệnh có thể được đặt bằng -tên tạp chí tùy chọn.

-tên tạp chí tên
Đặt tên của tệp tạp chí (không có .ml gia hạn). Mặc định là
frama_c_journal.

-initialized-padding-local
Khởi tạo ngầm định các local đặt các bit đệm thành 0. Nếu sai, các bit đệm
không được khởi tạo (mặc định là có).

[-no] -keep-comment
Cố gắng giữ lại các bình luận khi in mã nguồn khá đẹp (mặc định là không).

[-không] -giữ-chuyển-đổi
Thời Gian -đơn giản hóa-cfg được thiết lập, giữ các câu lệnh chuyển đổi. Mặc định là không.

-giữ-không-sử-dụng-cụ-thể-chức-năng
Xem -xem-không-dùng-được-chỉ-định-các-chức-năng

[-no] -lib-entry
Chỉ ra rằng điểm vào được gọi trong quá trình thực hiện chương trình. Điều này ngụ ý trong
đặc biệt là các biến toàn cục không thể được giả định là có các giá trị ban đầu của chúng.
Mặc định là -no-lib-entry: điểm vào cũng là điểm bắt đầu của
chương trình và toàn cầu có giá trị ban đầu của chúng.

tải hồ sơ
tải trạng thái (đã lưu trước đó) có trong hồ sơ.

-load-mô-đun m1 [, m2 [..., mn]]
tải các mô-đun ocaml thông qua . Các mô-đun này phải .cmxscác tập tin cho
phiên bản mã gốc của Frama-c và .Làm saoor.cmatệp cho phiên bản bytecode (xem
phần Dynlink của hướng dẫn sử dụng Ocaml để biết thêm thông tin). Tất cả các mô-đun được
hiện trong các đường dẫn tìm kiếm plugin được tải tự động.

-load-script s1 [, s2, [..., sn]]
tải các tập lệnh ocaml thông qua . Các tập lệnh phải .mlcác tập tin. Họ
phải có thể biên dịch chỉ dựa vào thư viện chuẩn Ocaml và API của Frama-C. Nếu như
một số bước biên dịch tùy chỉnh là cần thiết, biên dịch chúng bên ngoài Frama-C và sử dụng
-load-mô-đun thay thế.

-machdep máy
sử dụng máy như cấu hình phụ thuộc vào máy hiện tại (kích thước của các
kiểu số nguyên, endiandness, ...). Danh sách các máy hiện được hỗ trợ là
có sẵn thông qua -machdep giúp đỡ Lựa chọn. Mặc định là x86_32

-chủ yếu f
bộ f như là điểm đầu vào của phân tích. Mặc định là 'chính'. Theo mặc định, nó là
được coi là điểm khởi đầu của chương trình đang phân tích. Sử dụng -lib-mục nhập if f
được cho là sẽ được gọi ở giữa cuộc hành quyết.

-văn bản
in một phiên bản mã bị xáo trộn (trong đó số nhận dạng ban đầu được thay thế
bằng cách vô nghĩa) và lối ra. Bảng tương ứng giữa bản gốc và mới
ký hiệu được giữ ở đầu kết quả.

-code hồ sơ
chuyển hướng mã in đẹp đến hồ sơ thay vì đầu ra tiêu chuẩn.

[-no] -orig-name
Trong giai đoạn chuẩn hóa, một số biến có thể được đổi tên khi khác
biến có cùng tên có thể cùng tồn tại (ví dụ: biến toàn cục và biến chính thức
tham số). Khi tùy chọn này được bật, một thông báo sẽ được in mỗi khi điều này xảy ra.
Mặc định là không.

[-no] -warn-ký-downcast
tạo cảnh báo khi các tín hiệu downcast đã ký có thể vượt quá phạm vi đích (mặc định là
không phải).

[-no] -warn-ký-tràn
tạo cảnh báo cho các hoạt động đã ký bị tràn (mặc định là có).

[-no] -warn-unsigned-downcast
tạo ra cảnh báo khi các âm thanh không được đăng ký có thể vượt quá phạm vi đích (mặc định
không).

[-no] -warn-unsigned-tràn
tạo báo động cho các hoạt động chưa được đánh dấu làm tràn (mặc định là không).

[-no] -pp-annot
xử lý trước chú thích. Điều này hiện chỉ có thể thực hiện được khi sử dụng gcc (hoặc GNU
cpp) bộ xử lý trước. Mặc định là không xử lý trước các chú thích.

[-no] -print
in khá đẹp mã nguồn như được chuẩn hóa bởi CIL (mặc định là không).

-print-libpath
xuất ra thư mục nơi cài đặt thư viện hạt nhân Frama-C

-print-path
bí danh của -print-share-path

-print-plugin-path
xuất ra thư mục nơi Frama-C tìm kiếm các plugin của nó (có thể bị ghi đè bởi
FRAMAC_PLUGIN biến và -add-path không bắt buộc)

-print-share-path
xuất ra thư mục nơi Frama-C lưu trữ dữ liệu của nó (có thể bị ghi đè bởi
FRAMAC_SHARE Biến đổi)

-xem-không-dùng-được-chỉ-định-các-chức-năng
giữ nguyên mẫu hàm có đặc điểm kỹ thuật ACSL nhưng không được sử dụng trong
mã số. Đây là mặc định. Các hàm có thuộc tính FRAMAC_BUILTIN luôn luôn
đã giữ.

-mảng an toàn
Đối với mảng hoặc mảng nhiều chiều là các trường bên trong cấu trúc, giả sử rằng
tất cả các quyền truy cập phải bị ràng buộc (được đặt theo mặc định). Tùy chọn ngược lại là -không an toàn-
mảng

-cứu hồ sơ
Lưu trạng thái của Frama-C vào hồ sơ sau khi các phân tích diễn ra.

[-no] -simplify-cfg
loại bỏ câu lệnh break, tiếp tục và chuyển đổi trước khi phân tích. Mặc định là không.

-sau đó cho phép người ta soạn các bản phân tích: lần chạy Frama-C đầu tiên sẽ xảy ra với các tùy chọn
trước -sau đó và lần chạy thứ hai sẽ được thực hiện với các tùy chọn sau -sau đó trên
dự án hiện tại từ lần chạy đầu tiên.

-sau đó-on dự án
Tương tự như -sau đó ngoại trừ lần chạy thứ hai được thực hiện trong dự án dự án Nếu không có như vậy
dự án tồn tại, Frama-C thoát ra với lỗi.

-thời gian hồ sơ
nối ngày và giờ của người dùng trong hồ sơ khi Frama-C thoát.

-đánh máy
buộc đánh máy các tệp nguồn. Tùy chọn này chỉ có liên quan nếu không có thêm
phân tích được yêu cầu (vì việc đánh máy sẽ ngầm xảy ra trước khi phân tích
được khởi chạy).

-ulevel n
các vòng lặp giải nén cú pháp n lần trước khi phân tích. Điều này có thể khá tốn kém
và một số plugin (ví dụ: phân tích giá trị) cung cấp các cách hiệu quả hơn để thực hiện
giống nhau cả thôi. Xem hướng dẫn sử dụng tương ứng của họ để biết thêm thông tin. Điều này cũng có thể
được kích hoạt trên cơ sở mỗi vòng lặp thông qua vòng lặp thực dụng bỏ cuộn chỉ thị. A
giá trị âm cho n sẽ ức chế các pragmas như vậy.

[-no] -unicode
xuất ra các công thức ACSL với ký tự utf8. Đây là mặc định. Khi đưa ra
-không có unicode tùy chọn, Frama-C sẽ sử dụng phiên bản ASCII để thay thế. Xem hướng dẫn sử dụng ACSL
cho thư từ.

-mảng an toàn
xem -mảng an toàn

[-no] -không chỉ định-truy cập
kiểm tra xem các truy cập đọc / ghi có diễn ra theo thứ tự không xác định (theo C
khái niệm của tiêu chuẩn về điểm trình tự) được thực hiện trên các vị trí riêng biệt. Với
-không-không-xác-định-truy cập, giả sử rằng nó luôn luôn như vậy (đây là trường hợp mặc định).

-phiên bản
xuất ra chuỗi phiên bản của Frama-C

-warn-thập phân-float
cảnh báo khi không thể biểu diễn chính xác hằng số dấu phẩy động (ví dụ: 0.1).
có thể là một trong số không ai, hàng loạt, hoặc là tất cả các

[-no] -warn-undeclared-callee
cảnh báo khi một hàm được gọi trước khi nó được khai báo (đặt theo mặc định).
Frama-C

bổ sung riêng lựa chọn

Cho mỗi Plugin, lệnh

frama-c -Plugin-Cứu giúp

sẽ cung cấp danh sách các tùy chọn dành riêng cho plugin.

EXIT TÌNH TRẠNG

0 Thực hiện thành công

1 Đầu vào của người dùng không hợp lệ

2 Người dùng bị gián đoạn (giết hoặc tương đương)

3 Tính năng hợp nhất

4 5 6 Lỗi bên trong

125 Lỗi không thể nhận biết

Trạng thái thoát lớn hơn 2 có thể được coi là lỗi (hoặc yêu cầu tính năng cho trường hợp
của trạng thái thoát 3) và có thể được báo cáo trên Frama-C's BTS (xem bên dưới).

MÔI TRƯỜNG BIẾN

Có thể kiểm soát những nơi mà Frama-C tìm kiếm các tệp của nó thông qua
các biến sau.

FRAMAC_LIB
Thư mục nơi các giao diện đã biên dịch của hạt nhân được cài đặt

FRAMAC_PLUGIN
Thư mục mà Frama-C có thể tìm thấy các trình cắm thêm tiêu chuẩn. Nếu bạn muốn có plugin
ở một số nơi, sử dụng -add-path thay thế.

FRAMAC_SHARE
Thư mục chứa dữ liệu Frama-C được cài đặt.

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