如何用frama-c命令处理printf("")和scanf("")? [英] How to handle printf(" ", ) and scanf(" ") with frama-c command?
本文介绍了如何用frama-c命令处理printf("")和scanf("")?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我使用这段代码来生成一个C程序的控制流图。除了内置函数(如 printf
和 scanf
)外,它对所有函数都可以正常工作。我可以在这段代码中更改以输出内置函数吗?
I am using this code to generate the control flow graph of a C program. It is working fine for all the function except built-in function like printf
and scanf
. What can I change in this code to output the built in function as it is?
open Cil
open Cil_types
let print_stmt out =
function
| Instr i -> !Ast_printer.d_instr out i
| Return _ -> Format.pp_print_string out "<return>"
| Goto _ -> Format.pp_print_string out "<goto>"
| Break _ -> Format.pp_print_string out "<break>"
| Continue _ -> Format.pp_print_string out "<continue>"
| 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 "<loop>"
| Block _ -> Format.fprintf out "<enter block>"
| UnspecifiedSequence _ -> Format.fprintf out "<enter unspecified sequence>"
| TryFinally _ | TryExcept _ -> Format.fprintf out "<try>"
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 "@[<hov 2>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 "@[<hov 2>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
推荐答案
变量函数本身,而是字面字符串。您必须引用它们,否则点
认为标签已结束。尝试替换
The problem is not related to variadic functions per se, but instead to literal strings. You must quote them, as otherwise dot
thinks the label has ended. Try replacing
Format.fprintf out "s%d@[[label=\"%a\"]@];@\n" s.sid print_stmt s.skind;
by
Format.fprintf out "s%d@[[label=%S]@];@\n" s.sid (Pretty_utils.to_string print_stmt s.skind);
(请注意%S
,即输出一个带引号的字符串。)
(Notice the %S
, that outputs a quoted string.)
这篇关于如何用frama-c命令处理printf("")和scanf("")?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文