Add TODOs to ptranal

goblint · Jan 22, 2024 · 808b5d2 · 808b5d2
1 parent 271cc17
commit 808b5d2
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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