Merge pull request #1079 from goblint/libfuns-spec

Convert library functions to new specifications
goblint · Aug 3, 2023 · babc881 · babc881
2 parents d85c72e + ed231fa
commit babc881
Show file tree

Hide file tree

Showing 2 changed files with 380 additions and 359 deletions.
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
@@ -44,7 +44,7 @@ struct
   let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
     if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)\n" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
     if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then (
-      if deref then
+      if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *)
         do_access ctx kind reach exp;
       if M.tracing then M.tracei "access" "distribute_access_exp\n";
       Access.distribute_access_exp (do_access ctx Read false) exp;