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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001187 | Frama-C | Plug-in > aoraï | public | 2012-06-04 | 2012-09-19 |
| Reporter | nmuller | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
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.
