-
- Downloads
Merge branch 'fix/aorai/observed-backwards' into 'master'
[Aorai] support observables also in generated specs See merge request frama-c/frama-c!3510
No related branches found
No related tags found
Showing
- src/plugins/aorai/aorai_dataflow.ml 39 additions, 39 deletionssrc/plugins/aorai/aorai_dataflow.ml
- src/plugins/aorai/aorai_eva_analysis.enabled.ml 41 additions, 8 deletionssrc/plugins/aorai/aorai_eva_analysis.enabled.ml
- src/plugins/aorai/aorai_register.ml 7 additions, 4 deletionssrc/plugins/aorai/aorai_register.ml
- src/plugins/aorai/aorai_utils.ml 19 additions, 3 deletionssrc/plugins/aorai/aorai_utils.ml
- src/plugins/aorai/aorai_utils.mli 5 additions, 0 deletionssrc/plugins/aorai/aorai_utils.mli
- src/plugins/aorai/aorai_visitors.ml 60 additions, 96 deletionssrc/plugins/aorai/aorai_visitors.ml
- src/plugins/aorai/tests/ya/observed.i 20 additions, 0 deletionssrc/plugins/aorai/tests/ya/observed.i
- src/plugins/aorai/tests/ya/observed.ya 8 additions, 0 deletionssrc/plugins/aorai/tests/ya/observed.ya
- src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle 1 addition, 2 deletionssrc/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
- src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle 1 addition, 3 deletionssrc/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
- src/plugins/aorai/tests/ya/oracle/observed.res.oracle 383 additions, 0 deletionssrc/plugins/aorai/tests/ya/oracle/observed.res.oracle
- src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle 1 addition, 3 deletionssrc/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
- src/plugins/aorai/tests/ya/oracle_prove/observed.res.oracle 3 additions, 0 deletionssrc/plugins/aorai/tests/ya/oracle_prove/observed.res.oracle
Loading
Please register or sign in to comment