Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Re-exported variant is incorrectly marked dead #153

Open
sim642 opened this issue May 17, 2022 · 1 comment
Open

Re-exported variant is incorrectly marked dead #153

sim642 opened this issue May 17, 2022 · 1 comment

Comments

@sim642
Copy link

sim642 commented May 17, 2022

Running reanalyze 389dd68 on Goblint goblint/analyzer@a544002 revealed the following.

In MyCFG module we have the following re-exporting type definition:

(** Re-exported [Edge.t] with constructors. See [Edge.t] for documentation. *)
type edge = Edge.t =
  | Assign of CilType.Lval.t * CilType.Exp.t
  | Proc of CilType.Lval.t option * CilType.Exp.t * CilType.Exp.t list
  | Entry of CilType.Fundec.t
  | Ret of CilType.Exp.t option * CilType.Fundec.t
  | Test of CilType.Exp.t * bool
  | ASM of string list * Edge.asm_out * Edge.asm_in
  | VDecl of CilType.Varinfo.t
  | Skip

and in Edge module we have the original type definition:

type t =
  | Assign of CilType.Lval.t * CilType.Exp.t
  (** Assignments lval = exp *)
  | Proc of CilType.Lval.t option * CilType.Exp.t * CilType.Exp.t list
  (** Function calls of the form lva = fexp (e1, e2, ...) *)
  | Entry of CilType.Fundec.t
  (** Entry edge that relates function declaration to function body. You can use
    * this to initialize the local variables. *)
  | Ret of CilType.Exp.t option * CilType.Fundec.t
  (** Return edge is between the return statement, which may optionally contain
    * a return value, and the function. The result of the call is then
    * transferred to the function node! *)
  | Test of CilType.Exp.t * bool
  (** The true-branch or false-branch of a conditional exp *)
  | ASM of string list * asm_out * asm_in
  (** Inline assembly statements, and the annotations for output and input
    * variables. *)
  | VDecl of CilType.Varinfo.t
  (** VDecl edge for the variable in varinfo. Whether such an edge is there for all
    * local variables or only when it is not possible to pull the declaration up, is
    * determined by alwaysGenerateVarDecl in cabs2cil.ml in CIL. One case in which a VDecl
    * is always there is for VLA. If there is a VDecl edge, it is where the declaration originally
    * appeared *)
  | Skip [@dead "t.Skip"] 
  (** This is here for historical reasons. I never use Skip edges! *)

Despite the last documentation comment, we use MyCFG.Skip in various places and it's not marked dead. But the corresponding Edge.Skip variant is marked dead.
This is incorrect, because due to the type re-exporting, it wouldn't be possible to remove Edge.Skip as the two type manifests must match for the code to compile. I suppose reanalyze isn't accounting for this fact.

@cristianoc
Copy link
Collaborator

I think there's no attempt in the implementation to handle re-exported variants at the moment.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants