diff --git a/src/plugins/alias/src/abstract_state.ml b/src/plugins/alias/src/abstract_state.ml index 7e07ea865f47c9037b2eeeda17e2364363887524..25308698c088c279f5526b761cebb1e968ac2c5d 100644 --- a/src/plugins/alias/src/abstract_state.ml +++ b/src/plugins/alias/src/abstract_state.ml @@ -159,7 +159,13 @@ module Readout = struct assert (G.mem_vertex s.graph v); (* cycles can occur with unsafe casts such as: x->f = (int* ) x; *) let rec checking_for_cycles s visited v = - if VSet.mem v visited then LSet.empty else + if VSet.mem v visited then + let () = + Options.warning ~once:true ~wkey:Options.Warn.incoherent + "cycle during readout of vertex %d, \ + (following unsafe cast?); analysis may be unsound" v + in LSet.empty + else let visited = VSet.add v visited in let modified_predecessors = List.map (fun e -> @@ -290,7 +296,9 @@ let assert_invariants s : unit = G.iter_vertex assert_vertex s.graph; let assert_edge v1 v2 = Options.debug ~level:11 "checking coherence of edge %d → %d" v1 v2; - assert (v1 <> v2); + if v1 = v2 then + Options.warning ~once:true ~wkey:Options.Warn.incoherent + "loop on vertex %d (following unsafe cast?); analysis may be unsound" v1; assert (G.mem_vertex s.graph v1); assert (G.mem_vertex s.graph v2) in diff --git a/src/plugins/alias/src/options.ml b/src/plugins/alias/src/options.ml index 7c57801673f809e66add699feacd0ff7595c1bc4..ef9f63fa9464a7ed8aa9d50a17319cacc3723665 100644 --- a/src/plugins/alias/src/options.ml +++ b/src/plugins/alias/src/options.ml @@ -72,6 +72,7 @@ module Warn = struct let unsupported_asm = register_warn_category "unsupported:asm" let unsupported_function = register_warn_category "unsupported:fn" let unsafe_cast = register_warn_category "unsafe-cast" + let incoherent = register_warn_category "incoherent" end module DebugKeys = struct diff --git a/src/plugins/alias/src/options.mli b/src/plugins/alias/src/options.mli index bfe5800b537c1a318d743ab9f19ba389a1031700..603c67bcb21e5ee8e0be6001c2b7e4179fb6a9c6 100644 --- a/src/plugins/alias/src/options.mli +++ b/src/plugins/alias/src/options.mli @@ -48,6 +48,7 @@ module Warn : sig val unsupported_asm : warn_category val unsupported_function : warn_category val unsafe_cast : warn_category + val incoherent : warn_category end module DebugKeys : sig diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..290c2dbe3ecff381c311ba3d005640bee0c2b1fa --- /dev/null +++ b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle @@ -0,0 +1,35 @@ +[kernel] Parsing reduce_by_valid.c (with preprocessing) +[kernel:typing:incompatible-pointer-types] reduce_by_valid.c:5: Warning: + casting function to int * +[kernel:typing:incompatible-pointer-types] reduce_by_valid.c:5: Warning: + casting function to int * +[alias] analysing function: f +[alias] analysing instruction: int *q = (int *)(& f); +[alias:unsafe-cast] reduce_by_valid.c:5: Warning: + unsafe cast from void (*)(void) to int * +[alias] May-aliases after instruction int *q = (int *)(& f); are <none> +[alias] May-alias graph after instruction int *q = (int *)(& f); is + 0:{ q } → 1:{ f } +[alias] analysing instruction: int *p = (int *)(& f); +[alias:unsafe-cast] reduce_by_valid.c:5: Warning: + unsafe cast from void (*)(void) to int * +[alias] May-aliases after instruction int *p = (int *)(& f); are { q; p } +[alias] May-alias graph after instruction int *p = (int *)(& f); is + 0:{ q } → 5:{ f } 4:{ p } → 5:{ f } +[alias] analysing instruction: p = (int *)(& q); +[alias:unsafe-cast] reduce_by_valid.c:6: Warning: + unsafe cast from int ** to int * +[alias:incoherent] Warning: + loop on vertex 5 (following unsafe cast?); analysis may be unsound +[alias:incoherent] Warning: + cycle during readout of vertex 5, (following unsafe cast?); analysis may be unsound +[alias] May-aliases after instruction p = (int *)(& q); are { *p; f; q; p } +[alias] May-alias graph after instruction p = (int *)(& q); is + 4:{ p } → 5:{ f; q } 5:{ f; q } → 5:{ f; q } +[alias] May-aliases at the end of function f: { *p; f; q; p } +[alias] May-alias graph at the end of function f: + 4:{ p } → 5:{ f; q } 5:{ f; q } → 5:{ f; q } +[alias] Summary of function f: + formals: locals: q→{ f; q } p→{ f; q } returns: <none> + state: { *p; f; q; p } +[alias] Analysis complete diff --git a/src/plugins/alias/tests/known_bugs/reduce_by_valid.c b/src/plugins/alias/tests/fixed_bugs/reduce_by_valid.c similarity index 100% rename from src/plugins/alias/tests/known_bugs/reduce_by_valid.c rename to src/plugins/alias/tests/fixed_bugs/reduce_by_valid.c