diff --git a/src/analyses/ptranalEvalFunvar.ml b/src/analyses/ptranalEvalFunvar.ml new file mode 100644 index 0000000000..3b3d04ed6d --- /dev/null +++ b/src/analyses/ptranalEvalFunvar.ml @@ -0,0 +1,59 @@ +(** Wrapper analysis to answer EvalFunvar query using Cil's pointer analysis. *) + +open GoblintCil +open Analyses + +module Spec = +struct + include Analyses.DefaultSpec + + let name () = "ptranal" + + module D = Lattice.Unit + module C = Lattice.Unit + + (* transfer functions *) + let assign ctx (lval:lval) (rval:exp) : D.t = + ctx.local + + let branch ctx (exp:exp) (tv:bool) : D.t = + ctx.local + + let body ctx (f:fundec) : D.t = + ctx.local + + let return ctx (exp:exp option) (f:fundec) : D.t = + ctx.local + + let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = + [ctx.local, ctx.local] + + let combine_env ctx lval fexp f args fc au f_ask = + au + + let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t = + ctx.local + + let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = + ctx.local + + let query ctx (type a) (q: a Queries.t): a Queries.result = + match q with + | Queries.EvalFunvar (Lval (Mem e, _)) -> + let funs = Ptranal.resolve_exp e in + List.fold_left (fun xs f -> Queries.LS.add (f, `NoOffset) xs) (Queries.LS.empty ()) funs + | _ -> Queries.Result.top q + + let startstate v = D.bot () + let threadenter ctx lval f args = [D.top ()] + let threadspawn ctx lval f args fctx = ctx.local + let exitstate v = D.top () + + let init _: unit = + Ptranal.analyze_file !Cilfacade.current_file; + Ptranal.compute_results false + +end + +let _ = + MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index f608698521..d8fcdcd09a 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -754,6 +754,7 @@ struct [v] | _ -> (* Depends on base for query. *) + M.debug ~category:Program "Dynamic function call through %a" d_exp e; let ls = ctx.ask (Queries.EvalFunvar e) in Queries.LS.fold (fun ((x,_)) xs -> x::xs) ls [] in diff --git a/tests/regression/33-constants/05-fun_ptranal.c b/tests/regression/33-constants/05-fun_ptranal.c new file mode 100644 index 0000000000..5ebaf24e22 --- /dev/null +++ b/tests/regression/33-constants/05-fun_ptranal.c @@ -0,0 +1,14 @@ +//PARAM: --set ana.activated '["constants", "ptranal"]' +// intentional explicit ana.activated to do tutorial in isolation +int f(int a, int b){ + int d = 3; + int z = a + d; + return z; +} + +int main(){ + int d = 0; + int (*fp)(int,int) = &f; + d = fp(2, 3); + return 0; +}