Add more categories to unsound/imprecise call messages

goblint · Sep 25, 2023 · 70f267b · 70f267b
1 parent 8336d28
commit 70f267b
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -1104,12 +1104,12 @@ struct
       if AD.mem Addr.UnknownPtr fp then begin
         let others = AD.to_var_may fp in
         if others = [] then raise OnlyUnknown;
-        M.warn ~category:Imprecise "Function pointer %a may contain unknown functions." d_exp fval;
+        M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval;
         dummyFunDec.svar :: others
       end else
         AD.to_var_may fp
     with SetDomain.Unsupported _ | OnlyUnknown ->
-      M.warn ~category:Unsound "Unknown call to function %a." d_exp fval;
+      M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval;
       [dummyFunDec.svar]
 
   (** Evaluate expression as address.
@@ -1970,7 +1970,7 @@ struct
     end
 
   let special_unknown_invalidate ctx ask gs st f args =
-    (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise "Unknown function ptr called");
+    (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise ~tags:[Category Call] "Unknown function ptr called");
     let desc = LF.find f in
     let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
     let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
@@ -776,16 +776,16 @@ struct
           end
         else begin
           let geq = if var_arg then ">=" else "" in
-          M.warn ~tags:[CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length;
+          M.warn ~category:Unsound ~tags:[Category Call; CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length;
           None
         end
       | _ ->
-        M.warn  ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f;
+        M.warn ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f;
         None
     in
     let funs = List.filter_map one_function functions in
     if [] = funs then begin
-      M.warn ~category:Unsound "No suitable function to be called at call site. Continuing with state before call.";
+      M.warn ~category:Unsound ~tags:[Category Call] "No suitable function to be called at call site. Continuing with state before call.";
       d (* because LevelSliceLifter *)
     end else
       common_joins ctx funs !r !spawns