diff --git a/src/analyses/ptranalAnalysis.ml b/src/analyses/ptranalAnalysis.ml new file mode 100644 index 0000000000..6991b5ea22 --- /dev/null +++ b/src/analyses/ptranalAnalysis.ml @@ -0,0 +1,31 @@ +(** CIL's {!GoblintCil.Ptranal} for function pointer evaluation ([ptranal]). + + Useful for sound analysis of function pointers without base. *) + +(* TODO: fix unsoundness on some bench repo examples: https://github.com/goblint/analyzer/pull/1063 *) + +open GoblintCil +open Analyses + +module Spec = +struct + include UnitAnalysis.Spec + + let name () = "ptranal" + + 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 + (* TODO: filter compatible function pointers by type? *) + List.fold_left (fun xs f -> Queries.AD.add (Queries.AD.Addr.of_var f) xs) (Queries.AD.empty ()) funs + | _ -> Queries.Result.top q + + 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/goblint_lib.ml b/src/goblint_lib.ml index 06c51b0c15..4b2eecb632 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -164,6 +164,7 @@ module TaintPartialContexts = TaintPartialContexts module UnassumeAnalysis = UnassumeAnalysis module ExpRelation = ExpRelation module AbortUnless = AbortUnless +module PtranalAnalysis = PtranalAnalysis (** {1 Domains} 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; +}