A very strange problem

ID0000241: This issue was created automatically from Mantis Issue 241. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000241	Frama-C	Plug-in > jessie	public	2009-09-11	2011-04-03

Reporter	damien	Assigned To	cmarche	Resolution	suspended
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Beryllium-20090901	Target Version	-	Fixed in Version	-

Description :

Hello,

I was trying to verify the following small piece of code. The problem I encountered is as follows.

The command "frama-c -jessie File.c" hangs on "Generating VCs" grabbing the 1Gb memory.

The command "frama-C -jessie-apt alt-ergo File.c" claims that IDENTIFIER1, IDENTIFIER2, .. are unbound logic variables.

Trying the code with a single variable and one identifier works.

Could you help? Thank you

Additional Information :

#include "some_BasicIO.h" //where IDENTIFIER1, ... are defined

bool_t var0_0; ... 22 other variables of the same type

/@ assigns var0_0, and the other 22 variables; ensures ID == IDENTIFIER1?var0_0 == IO_State: (ID == IDENTIFIER2?variable2 == IO_State: ...and all 21 others :\true )))))))))))))))))))))))));/ void FUNCTION_Assign(uint8_t ID, bool_t State) { switch(ID) { case IDENTIFIER1: p0_0 = State; break;

	case IDENTIFIER2: var0_1 = State; break;
		
	... and all the 21 other similar case statements
	default: break;
}

}