maps of structs

Sep 25, 2009 at 1:59 PM

Hi all!

I wonder if it is possible to define maps of C structures.

judging from my minimal example it does not seem to be supported...
in fact it caused VCC to crash...

#include "vcc.h"

spec(
	typedef struct S_str {
		unsigned int id;
	} S_t;
)

spec(
struct abs_str {
	bool Sset[S_t];

	invariant(Sset == lambda(S_t s; true ; s.id < 42))
} abs;
)

 

Coordinator
Sep 25, 2009 at 6:10 PM

I guess maps from structs are not supported, although I couldn't find it documented and there should be a proper error message.

(Maps from records are not supported, which is documented in http://vcc.codeplex.com/Wiki/View.aspx?title=Record%20types.)

I'll turn your post into a work item.

Coordinator
Sep 25, 2009 at 6:12 PM
This discussion has been copied to a work item. Click here to go to the work item and continue the discussion.