1
Vote

def functions with struct access dumps boogie

description

The following causes VCC to dump boogie:

typedef struct S {
int x;
} S;

_(def S foo() {
S s;
s.x = 3;
return s;
})

comments

erniecohen wrote Jun 19, 2012 at 3:38 AM

The following gets the error "error VC9600: OOPS: expected $struct type, got void for (@vs_updated((vs.s->x), 3)->x)" :

typedef struct S {
int x;
} S;

_(def S foo() {
S s;
s.x = 3;
s.x = 3;
return s;
})

MichalMoskal wrote Jul 31, 2012 at 12:36 AM

As a workaround, you can use records with def functions

Sign in to add a comment or to set email notifications