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"

	typedef struct S_str {
		unsigned int id;
	} S_t;

struct abs_str {
	bool Sset[S_t];

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


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

I'll turn your post into a work item.

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.