当前位置: 首页 > 工具软件 > Frama-C > 使用案例 >

linux中fprintf函数,linux-如何使用frama-c命令处理printf(“”,)和...

席银龙
2023-12-01

我正在使用此代码生成C程序的控制流程图.除内置功能(如printf和scanf)外,该功能对于所有功能均正常运行.我可以在此代码中进行哪些更改以按原样输出内置函数?

open Cil

open Cil_types

let print_stmt out =

function

| Instr i -> !Ast_printer.d_instr out i

| Return _ -> Format.pp_print_string out ""

| Goto _ -> Format.pp_print_string out ""

| Break _ -> Format.pp_print_string out ""

| Continue _ -> Format.pp_print_string out ""

| If (e,_,_,_) -> Format.fprintf out "if %a" !Ast_printer.d_exp e

| Switch(e,_,_,_) -> Format.fprintf out "switch %a" !Ast_printer.d_exp e

| Loop _ -> Format.fprintf out ""

| Block _ -> Format.fprintf out ""

| UnspecifiedSequence _ -> Format.fprintf out ""

| TryFinally _ | TryExcept _ -> Format.fprintf out ""

class print_cfg out =

object

inherit Visitor.frama_c_inplace

method vstmt_aux s =

Format.fprintf out "s%d@[[label=\"%a\"]@];@\n" s.sid print_stmt s.skind;

List.iter

(fun succ -> Format.fprintf out "s%d -> s%d;@\n" s.sid succ.sid)

s.succs;

DoChildren

method vglob_aux g =

match g with

| GFun(f,loc) ->

Format.fprintf out "@[subgraph cluster_%a {@\n\

graph [label=\"%a\"];@\n"

Cil_datatype.Varinfo.pretty f.svar

Cil_datatype.Varinfo.pretty f.svar;

ChangeDoChildrenPost([g], fun g -> Format.fprintf out "}@\n@]"; g)

| _ -> SkipChildren

method vfile f =

Format.fprintf out "@[digraph cfg {@\n";

ChangeDoChildrenPost (f,fun f -> Format.fprintf out "}@."; f)

end

let run () =

let chan = open_out "cfg.out" in

let fmt = Format.formatter_of_out_channel chan in

Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get())

let () = Db.Main.extend run

 类似资料: