Skip to content

Memory "softcoding": regression on equivalences #819

@loutr

Description

@loutr

Regression introduced by commit 23cf445. MWE:

type t.

module M = {
  var tf, tg : t 

  proc f() = {
    var x;
    x <- tf;
    return x;
  }

  proc g() = {
    var x;
    x <- tg;
    return x;
  }
}.

equiv fg : M.f ~ M.g : M.tf{1} = M.tg{2} ==> ={res}.
proc. (* anomaly: Failure("expecting memory") *)

Replacing the function bodies by return tf;/return tg; makes the proc tactic go through.

I'll try to investigate if I have some time. But I believe this is not the only regression introduced by this commit.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type
No fields configured for issues without a type.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions