state chart implemented in multiple files cannot be analysed by aorai
ID0001187: This issue was created automatically from Mantis Issue 1187. Further discussion may take place here.
|ID0001187||Frama-C||Plug-in > aoraï||public||2012-06-04||2012-09-19|
|Reporter||nmuller||Assigned To||virgile||Resolution||no change required|
|Product Version||Frama-C Nitrogen-20111001||Target Version||-||Fixed in Version||Frama-C Oxygen-20120901|
It seems not possible to check a state-chart that would be implemented in multiple c files (as a consequence of modular design). We tried to submit a small project to aorai, but the tool was not able to accept a semantic on multiple files.
It is not possible apparently to capture in a sole ltl file the description of a state-chart which would be able to link all the called states.