[Aorai] Add a list of observables
- add an "observables" option at the begining of ya files - multiple "observables" options merges together (union of symbols) - check that every function referred to is inside the observable list - remove the initial curOperation and curOpStatus : the main function is not necessarily observable and the pre/post function will set those variables anyway - ignore unobservables functions inside the relevant visitors
Showing
- src/plugins/aorai/aorai_dataflow.ml 6 additions, 6 deletionssrc/plugins/aorai/aorai_dataflow.ml
- src/plugins/aorai/aorai_utils.ml 20 additions, 36 deletionssrc/plugins/aorai/aorai_utils.ml
- src/plugins/aorai/aorai_visitors.ml 91 additions, 85 deletionssrc/plugins/aorai/aorai_visitors.ml
- src/plugins/aorai/data_for_aorai.ml 50 additions, 32 deletionssrc/plugins/aorai/data_for_aorai.ml
- src/plugins/aorai/data_for_aorai.mli 9 additions, 9 deletionssrc/plugins/aorai/data_for_aorai.mli
- src/plugins/aorai/promelaast.mli 1 addition, 0 deletionssrc/plugins/aorai/promelaast.mli
- src/plugins/aorai/promelaparser.mly 9 additions, 2 deletionssrc/plugins/aorai/promelaparser.mly
- src/plugins/aorai/promelaparser_withexps.mly 9 additions, 2 deletionssrc/plugins/aorai/promelaparser_withexps.mly
- src/plugins/aorai/tests/ltl/oracle/goto.res.oracle 2 additions, 2 deletionssrc/plugins/aorai/tests/ltl/oracle/goto.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle 2 additions, 2 deletionssrc/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle 2 additions, 2 deletionssrc/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle 2 additions, 2 deletionssrc/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle 2 additions, 2 deletionssrc/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle 2 additions, 2 deletionssrc/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle 2 additions, 2 deletions...plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle 2 additions, 2 deletions...ugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle 2 additions, 2 deletions...ugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle 2 additions, 2 deletionssrc/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle 2 additions, 2 deletionssrc/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
- src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle 2 additions, 2 deletions...rai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
Loading
Please register or sign in to comment