Có thể sử dụng frama-c để phân tích tệp tiêu đề không?

Question

Tôi đã xem xét frama-c như một cách để xử lý các tệp tiêu đề C trong OCaml (ví dụ: để tạo các ràng buộc ngôn ngữ). Nó hấp dẫn bởi vì nó có vẻ giống như một dự án được lưu trữ rất tốt và duy trì. Tuy nhiên, sau rất nhiều googling và tìm kiếm thông qua các tài liệu, tôi không thể tìm thấy bất cứ điều gì phù hợp cho mục đích này. Tôi chỉ thiếu đúng cách để làm điều này, hay nó nằm ngoài phạm vi của frama-c? Nó có vẻ như một điều khá tầm thường cho nó để làm, so với một số các plugin khác.

Answer 1

Như Pascal nói, tôi không nghĩ rằng nó có thể từ dòng lệnh, nhưng vì bạn sẽ phải viết một số mã, bạn có thể đặt cờ Rmtmps.keepUnused. Đây là một kịch bản mà bạn có thể sử dụng để xem các tờ khai:

let main() = 
    Rmtmps.keepUnused := true; 
    let file = File.from_filename "t.h" in 
    let() = File.init_from_c_files [ file ] in 
    let _ast = Ast.get() in 
    let show_function f = 
    let name = Kernel_function.get_name f in 
    if not (Cil.Builtin_functions.mem name) then 
     Format.printf "Function @[<2>%a:@ @[@[type: %a@]@ @[%s at %a@]@]@]@." 
     Kernel_function.pretty f 
     Cil_datatype.Typ.pretty (Kernel_function.get_type f) 
     (if Kernel_function.is_definition f then "defined" else "declared") 
     Cil.d_loc (Kernel_function.get_location f) 
in Globals.Functions.iter show_function 

let() = Db.Main.extend main 

Để chạy nó, bạn phải sử dụng tùy chọn -load-script như thế này:

$ frama-c -load-script script.ml 

đang phát triển một plug-in sẽ phù hợp hơn để xử lý phức tạp hơn (xem Hướng dẫn dành cho nhà phát triển cho điều đó), nhưng một tập lệnh giúp bạn dễ dàng kiểm tra.

Answer 2

Trong trạng thái hiện tại, tôi có thể nói rằng rất tiếc là không thể sử dụng Frama-C để phân tích cú pháp các khai báo hàm không được xác định hoặc sử dụng.

t.h:

int mybinding (int x, int y); 

này cung cấp cho bạn một cái nhìn của AST bình thường. Bình thường có nghĩa là tất cả những gì có thể được đơn giản hóa là:

$ frama-c -print t.h 
[kernel] preprocessing with "gcc -C -E -I. t.h" 
/* Generated by Frama-C */ 

Và thật không may, vì mybinding đã không sử dụng cũng không được xác định, nó đã bị xóa.

Có một tùy chọn để giữ cho các khai báo có thông số kỹ thuật, nhưng những gì bạn muốn là một tùy chọn để giữ tất cả các khai báo. Tôi chưa bao giờ thấy một tùy chọn như:

$ frama-c -kernel-help 
... 
-keep-unused-specified-functions keep specified-but-unused functions (set by 
        default, opposite option is 
        -remove-unused-specified-functions) 

Và tùy chọn để giữ chức năng với thông số kỹ thuật không làm những gì bạn muốn:

$ frama-c -keep-unused-specified-functions -print t.h 
[kernel] preprocessing with "gcc -C -E -I. t.h" 
/* Generated by Frama-C */