unable to use lemma separated_region
ID0002041: This issue was created automatically from Mantis Issue 2041. Further discussion may take place here.
|ID0002041||Frama-C||Plug-in > wp||public||2014-12-28||2015-06-29|
|Product Version||Frama-C Neon-20140301||Target Version||-||Fixed in Version||-|
I am using two Frama-C installation:
1.) Neon-20140301 installed through opam under OS X 2.) Neon-20140301+dev-stance manually installed under Linix
In both installations the lemma separated_region in file FRAMAC_SHARE/wp/coqwp/Memory.v is unaccessible because it is put in comments. I suspect that this is the reason why I cannot prove that a local struct variable is separated from one that a function receives as an argument.
What is the reason that this lemma is not available?