我从Frama-c开始，所以我不能很好地掌握它。我想使用Frama-c来实现指针别名分析器。除非我弄错了，否则在我看来，值插件不会提供有关指针别名的信息。
首先，我有以下内容：
class vtest = object(self)
inherit Visitor.frama_c_inplace as super
method private try_khow_exp_from_inst vi loc exp (typ : string) =
let vname = vi.vname in
match exp.enode with
| Const _ | SizeOfE _ | AlignOfE _ | SizeOf _ | AlignOf _ | SizeOfStr _->
Format.printf "Local %s of #%s# (of type %a) with a constant (%a) at %a @.\n"
typ vname Printer.pp_typ vi.vtype Printer.pp_exp exp Printer.pp_location loc;
if Cil.isPointerType vi.vtype then
Format.printf "#%s# is a pointer type !!! warning: initialization makes pointer from integer without a cast @.\n" vname;
| Lval(Var v, _) ->
Format.printf "Local %s of #%s# with a variable (%s) at %a @.\n"
typ vname v.vname Printer.pp_location loc;
if Cil.isPointerType vi.vtype && Cil.isPointerType v.vtype then
Format.printf "Pointer #%s# is aliased with pointer (%s) --> #%s# can't be declared as restrict neither (%s) @.\n"
vname v.vname vname v.vname;
| Lval (Mem e, _) ->
let state = Db.Value.get_state (Kstmt (Extlib.the self#current_stmt)) in
Format.printf "Local %s of variable #%s# with the value pointed by (%a) pointer at %a @.\n"
typ vname Printer.pp_exp e Printer.pp_location loc;
| UnOp(op, {enode = Lval (Mem {enode = Lval(Var v_un, _)}, _)}, _) when Cil.isPointerType v_un.vtype ->
Format.printf "Local %s of variable #%s# with an unary operation on pointer (%s) at %a @.\n"
typ vname v_un.vname Printer.pp_location loc;
| BinOp((PlusPI | IndexPI | MinusPI | MinusPP), {enode = Lval(Var v_ptr, _)}, e2, _) ->
if Cil.isPointerType vi.vtype && Cil.isPointerType v_ptr.vtype then
begin
Format.printf "Local %s of pointer #%s# with pointer (%s) +|- an offset at %a @.\n"
typ vname v_ptr.vname Printer.pp_location loc;
Format.printf "Pointer #%s# is aliased with pointer (%s) --> #%s# can't be declared as restrict neither (%s) @.\n"
vname v_ptr.vname vname v_ptr.vname;
end
| StartOf(Var va, _) when Cil.isPointerType vi.vtype ->
Format.printf "Local %s of pointer #%s# with start addr of array (%s) at %a @.\n" typ vname va.vname Printer.pp_location loc;
Format.printf "Pointer #%s# is aliased with array (%s) --> #%s# can't be declared as restrict@.\n"
vname va.vname vname;
| AddrOf(Var v_ad, _) when Cil.isPointerType vi.vtype ->
Format.printf "Local %s of pointer #%s# with address of variable (%s) at %a @.\n"
typ vname v_ad.vname Printer.pp_location loc;
Format.printf "Pointer #%s# is aliased with variable (%s) --> #%s# can't be declared as restrict @.\n"
vname v_ad.vname vname;
| _ -> Format.printf "Found unknow case at %a...@.\n" Printer.pp_location loc;
method private do_call var f args l =
let kf = Globals.Functions.get f in
let name = Kernel_function.get_name kf in
let params = Globals.Functions.get_params kf in
Format.printf "Local init of #%s# at %a: through a call to (%s) with following params --> @."
var.vname Printer.pp_location l name;
if params != [] then List.iter(fun vi ->
let lval = (Var vi, NoOffset) in (* make an lval from a varinfo *)
let loc = !Db.Value.lval_to_loc self#current_kinstr ~with_alarms:CilE.warn_none_mode lval in
Db.Value.fold_state_callstack (fun state () -> (* for each state in the callstack *)
let value = Db.Value.find state loc in (* obtain value for location *)
Format.printf "%a -> %a@." Printer.pp_varinfo vi
Locations.Location_Bytes.pretty value (* print mapping *)
) () ~after:true self#current_kinstr
) params;
Format.printf "@.\n"
method! vinst i =
if Db.Value.is_reachable (Db.Value.get_state self#current_kinstr) then
match i with
| Local_init (vi, AssignInit(SingleInit e), loc) ->
let t = "init" in
self#try_khow_exp_from_inst vi loc e t;
Cil.SkipChildren
(*| Local_init (ci, AssignInit(CompoundInit _), loc)*)(**ToDo*)
| (Local_init(v, ConsInit(f, args, k), l)) when Cil.isPointerType v.vtype -> begin
match k with
| Plain_func -> self#do_call v f args l ; Cil.SkipChildren
| Constructor -> Cil.SkipChildren
end
| Set((Var(vi),NoOffset), exp, place) ->
let s = "setting" in
self#try_khow_exp_from_inst vi place exp s;
Cil.SkipChildren
| Call(Some(Var call, _), {enode = Lval(Var vfunc, _)}, argl, lsome) ->
Format.printf "Call to (%s) and result is the lval #%s# at %a @." vfunc.vname call.vname Printer.pp_location lsome;
Format.printf "Function (%s) is called with following params: @.\n" vfunc.vname;
if argl != [] then
List.iter (fun exp -> match exp.enode with
| Lval(Var e, _) when Cil.isPointerType e.vtype -> Format.printf "pointer #%s# " e.vname;
| Lval(Var e, _) when not( Cil.isPointerType e.vtype || Cil.isArrayType e.vtype) ->
Format.printf "variable #%s# " e.vname;
| Lval(Var e, _) when Cil.isArrayType e.vtype -> Format.printf "static array #%s# " e.vname;
| AddrOf(Var v_ad, _) -> Format.printf "variable #%s# " v_ad.vname;
| _ -> ()
) argl;
Format.printf "@.\n";
Cil.SkipChildren
| Call(None, {enode = Lval(Var vfunc, _)}, argl, lnone) ->
Format.printf "Call to (%s) at %a with following params: @.\n" vfunc.vname Printer.pp_location lnone;
if argl != [] then
List.iter (fun exp -> match exp.enode with
| Lval(Var e, _) when Cil.isPointerType e.vtype -> Format.printf "pointer #%s# " e.vname;
| Lval(Var e, _) when not( Cil.isPointerType e.vtype || Cil.isArrayType e.vtype) ->
Format.printf "variable #%s# " e.vname;
| Lval(Var e, _) when Cil.isArrayType e.vtype -> Format.printf "static array #%s# " e.vname;
| AddrOf(Var v_ad, _) -> Format.printf "variable #%s# " v_ad.vname;
| _ -> ()
) argl;
Format.printf "@.\n";
Cil.SkipChildren
| _ -> Cil.DoChildren
else begin
Format.printf "Not reachable by Db.Value ...@.";
Cil.SkipChildren
end
initializer !Db.Value.compute();
end
使用这个脚本，我可以检测到一些指针别名的情况。但是，对于带有malloc的动态分配数组，我遇到了一些困难。
以这个小程序为例：
int main(int argc, char** argv) {
int n = 20;
int *a = malloc(n * sizeof(int));
int *b = malloc(n * sizeof(int));
int i;
for(i = 0; i<n; i++)
*(a + i) = 14 + i;
return 0;
}
当我使用-deref选项启动inout插件时，我可以看到两个值消息：
/home/rokiatou/Documents/frama-c-scripts/test.c:11:[value]分配变量__malloc_main_l11
/home/rokiatou/Documents/frama-c-scripts/test.c:12:[value]分配变量__malloc_main_l12
这些inout插件的消息：
函数main的[inout] Derefs：__ malloc_main_l11 [0..19]
我在4.6.4节中阅读了值插件指南：
动态分配通过创建新基础来建模。每次调用malloc和realloc都可能会创建一个新的基础。
在第8.1.1节中，重写此表单的消息：
[value]分配变量__malloc_main_l42_2981
表明正在创建新的基地。
所以我的问题是：
1）如何访问由值分配的变量__malloc*的基址，并将其与我的源代码中存在的实变量相关联（例如，变量a和b）？
2）如何获得malloc函数分配的元素数量（在我的例子中，它是n (=20)）？
我已经查看了文件cil_types.mli（我发现了TPtr和TArray类型）和base.mli，但我并不真正理解它们的用法。
你想要达到的目标并不是很清楚，但是你的do_call方法中有几点看起来很可疑：
int *x = malloc (sizeof(*x));和x = malloc(sizeof(*x));。换句话说，你可以将Local_init（与Cons_init）和Call案例之间的大部分工作分解。malloc，calloc和realloc在这里是相关的。args列表中的表达式而不是varinfo列表中的params。