Merge branch 'fix/ghost/result_type' into 'master'
[kernel] fix \result type for ghost functions See merge request frama-c/frama-c!3778
No related branches found
No related tags found
Showing
- src/kernel_internals/typing/ghost_accesses.ml 1 addition, 1 deletionsrc/kernel_internals/typing/ghost_accesses.ml
- src/kernel_services/ast_data/kernel_function.ml 2 additions, 0 deletionssrc/kernel_services/ast_data/kernel_function.ml
- src/kernel_services/ast_data/kernel_function.mli 18 additions, 0 deletionssrc/kernel_services/ast_data/kernel_function.mli
- src/kernel_services/ast_queries/cil.mli 5 additions, 0 deletionssrc/kernel_services/ast_queries/cil.mli
- src/kernel_services/ast_queries/filecheck.ml 4 additions, 0 deletionssrc/kernel_services/ast_queries/filecheck.ml
- src/kernel_services/ast_queries/logic_typing.ml 4 additions, 1 deletionsrc/kernel_services/ast_queries/logic_typing.ml
- src/plugins/aorai/aorai_utils.ml 3 additions, 2 deletionssrc/plugins/aorai/aorai_utils.ml
- tests/spec/ghost_result_type.i 14 additions, 0 deletionstests/spec/ghost_result_type.i
- tests/spec/oracle/ghost_result_type.res.oracle 23 additions, 0 deletionstests/spec/oracle/ghost_result_type.res.oracle
Loading
Please register or sign in to comment