Union support

[Mark Tuttle]

Do you have advice on verifying code with unions?

If I run `verifast test1.c` on

#include <stdint.h>

typedef union

{

    char c;

    uint8_t u;

} char_;

int main ()

//@ requires true;

//@ ensures true;

{

  char_ n;

  n.c = 'a';

  return 0;

}

then verifast points to the token "union" and says "A union type with a body is not supported in this position."

If I run `verifast test2.c` on 

#include <stdint.h>

union char_

{

    char c;

    uint8_t u;

};

int main ()

//@ requires true;

//@ ensures true;

{

  union char_ n;

  n.c = 'a';

  return 0;

}

then verifast points to the "." in "n.c" and says "Taking the address of this expression is not supported."

[Bart Jacobs]

I pushed a commit just now; these examples now verify.

Note: VeriFast produces a union object as just an array of chars, so when accessing a union member whose type is anything other than char, you first need to convert the array of chars to the desired type of chunk. See https://github.com/verifast/verifast/blob/master/examples/unions2.c .

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/8c0b4251-9816-4c8d-bab0-7f5311b93cfen%40googlegroups.com.