smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
427 stars 82 forks source link

Multi-language model checking, on inequality modify languages to match correct model? #771

Open SamuelMarks opened 2 years ago

SamuelMarks commented 2 years ago

So say I had something like this, with arbitrary languages supported by SMACK:


class Foo:
    @property
    bar: float

^Note the type of bar

class Foo {
public:
    int bar;
};
public class Foo {
    public int bar;
}
public class Foo {
   public int bar { get; set; }
};

Now I want to compare all the target languages, and point out which one has the 'wrong' structure. I'm confident SMACK can do this.

Next, I want to explicitly specify the right structure (e.g., bar should be float) and change all source files to match this new structure (rerunning SMACK as a sanity check that the structures are now equal).


AFAIK, SMACK doesn't support this workflow. Could you advise? (also advise if not SMACK then if you know of a project that facilitates this workflow)

Thanks