diff --git a/src/analyses/ptranalAnalysis.ml b/src/analyses/ptranalAnalysis.ml index d9352448c2..6991b5ea22 100644 --- a/src/analyses/ptranalAnalysis.ml +++ b/src/analyses/ptranalAnalysis.ml @@ -2,6 +2,8 @@ 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 @@ -15,6 +17,7 @@ struct 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