Merge branch 'feature/blanchard/ghost-qualifier' into 'master'
\ghost qualifier for typing of ghost code See merge request frama-c/frama-c!2377
No related branches found
No related tags found
Showing
- .Makefile.lint 0 additions, 2 deletions.Makefile.lint
- Makefile 1 addition, 0 deletionsMakefile
- headers/header_spec.txt 2 additions, 0 deletionsheaders/header_spec.txt
- src/kernel_internals/parsing/clexer.mll 10 additions, 0 deletionssrc/kernel_internals/parsing/clexer.mll
- src/kernel_internals/parsing/cparser.mly 13 additions, 2 deletionssrc/kernel_internals/parsing/cparser.mly
- src/kernel_internals/typing/cabs2cil.ml 15 additions, 0 deletionssrc/kernel_internals/typing/cabs2cil.ml
- src/kernel_internals/typing/ghost_accesses.ml 250 additions, 0 deletionssrc/kernel_internals/typing/ghost_accesses.ml
- src/kernel_internals/typing/ghost_accesses.mli 29 additions, 0 deletionssrc/kernel_internals/typing/ghost_accesses.mli
- src/kernel_internals/typing/oneret.ml 3 additions, 1 deletionsrc/kernel_internals/typing/oneret.ml
- src/kernel_services/ast_data/kernel_function.ml 6 additions, 2 deletionssrc/kernel_services/ast_data/kernel_function.ml
- src/kernel_services/ast_data/kernel_function.mli 5 additions, 1 deletionsrc/kernel_services/ast_data/kernel_function.mli
- src/kernel_services/ast_printing/cabs_debug.ml 1 addition, 0 deletionssrc/kernel_services/ast_printing/cabs_debug.ml
- src/kernel_services/ast_printing/cil_printer.ml 10 additions, 0 deletionssrc/kernel_services/ast_printing/cil_printer.ml
- src/kernel_services/ast_printing/cprint.ml 1 addition, 0 deletionssrc/kernel_services/ast_printing/cprint.ml
- src/kernel_services/ast_queries/cil.ml 58 additions, 36 deletionssrc/kernel_services/ast_queries/cil.ml
- src/kernel_services/ast_queries/cil.mli 201 additions, 186 deletionssrc/kernel_services/ast_queries/cil.mli
- src/kernel_services/parsetree/cabs.ml 118 additions, 118 deletionssrc/kernel_services/parsetree/cabs.ml
- src/kernel_services/plugin_entry_points/kernel.ml 3 additions, 0 deletionssrc/kernel_services/plugin_entry_points/kernel.ml
- src/kernel_services/plugin_entry_points/kernel.mli 4 additions, 0 deletionssrc/kernel_services/plugin_entry_points/kernel.mli
- src/plugins/e-acsl/src/code_generator/injector.ml 7 additions, 2 deletionssrc/plugins/e-acsl/src/code_generator/injector.ml
Loading
Please register or sign in to comment