[kernel] working -inline-calls
Tested with function having arguments and recursive functions
Showing
- src/kernel_services/ast_data/kernel_function.ml 36 additions, 24 deletionssrc/kernel_services/ast_data/kernel_function.ml
- src/kernel_services/ast_data/kernel_function.mli 5 additions, 0 deletionssrc/kernel_services/ast_data/kernel_function.mli
- src/kernel_services/ast_queries/cil.ml 1 addition, 0 deletionssrc/kernel_services/ast_queries/cil.ml
- src/kernel_services/ast_queries/cil.mli 4 additions, 0 deletionssrc/kernel_services/ast_queries/cil.mli
- src/kernel_services/ast_transformations/inline.ml 125 additions, 159 deletionssrc/kernel_services/ast_transformations/inline.ml
- tests/syntax/inline_calls.i 8 additions, 1 deletiontests/syntax/inline_calls.i
- tests/syntax/oracle/inline_calls.res.oracle 67 additions, 16 deletionstests/syntax/oracle/inline_calls.res.oracle
Loading
Please register or sign in to comment