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. ## Attachments - [state_WP2.zip](/uploads/61f7dca1d4f9e758ee0bd53820b4dd7a/state_WP2.zip) - [WP2_Example.pdf](/uploads/f9b4b339e047d3bd596678b087adb061/WP2_Example.pdf) -