Kernel should desugar "complete behaviors"
ID0001006: This issue was created automatically from Mantis Issue 1006. Further discussion may take place here.
|Product Version||Frama-C Nitrogen-20111001||Target Version||-||Fixed in Version||Frama-C Oxygen-20120901|
Currently, the kernel does not transform "complete behaviors;" clauses into "complete behaviors b1 ... bn;" when it sees one. However, this would be worthwhile:
- it makes life simpler for all the plugins, that have one less case to handle
- if someone adds some named behaviors programmatically, the "complete behaviors;" clause becomes less precise.