search

kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

HavocAction does not handle destructor assignment #63

Open nano-o opened 2 years ago

nano-o commented 2 years ago

Here's an example:

#lang ivy1.7

type obj = struct {
    s : bool
}

individual my_obj: obj

after init {
    my_obj.s := false;
}

export action act = {
    var o:obj;
    o.s := *;
}

invariant my_obj.s = false

The invariant breaks when it should not.