File "verifast1.ml", line 301, characters 23-29: Assertion failed

[jameshfisher]

I get this error when attempting to verify a file:

$ ~/Downloads/verifast-16.01/bin/verifast rb_msg_store.c
rb_msg_store.c
Fatal error: exception File "verifast1.ml", line 301, characters 23-29: Assertion failed

Comes from https://github.com/verifast/verifast/blob/master/src/verifast1.ml#L301 :

    | StructType sn -> failwith "Using a struct as a value is not yet supported."

Seeing the message in the source I was quickly able to fix the error. Until this feature is added, can we ensure that the failure message is shown to the end user?

Btw @btj long time no speak! Very glad to see you're still working on VeriFast. And it's great to see that it's finally open source! (Because I wouldn't have been able to move past this error otherwise :-) )

[btj]

Hi James,

Yes, long time no speak :-) Glad to see you're still playing with VeriFast!

With respect to the issue: this was fixed by bec3035, post-release 16.01. I'll leave this issue open, though, as a reminder to produce a new release.

[jameshfisher]

Ah, great! I should try building from source.

I picked up VeriFast again at the weekend because we have some C code which is important, optimized for hot path, and has a nice logical interface, which is ideal for verification. I did a little research and it seems VeriFast is still the premier tool for C verification. (I also looked at Frama-C, which by comparison seems complex and ad hoc.)