Merge branch 'feature/blanchard/ghost-else' into 'master'
Supports ghost-else contruct See merge request frama-c/frama-c!2375
Showing
- .Makefile.lint 0 additions, 2 deletions.Makefile.lint
- Makefile 5 additions, 0 deletionsMakefile
- src/kernel_internals/parsing/clexer.mll 43 additions, 3 deletionssrc/kernel_internals/parsing/clexer.mll
- src/kernel_internals/parsing/cparser.mly 33 additions, 11 deletionssrc/kernel_internals/parsing/cparser.mly
- src/kernel_internals/typing/cabs2cil.ml 2 additions, 1 deletionsrc/kernel_internals/typing/cabs2cil.ml
- src/kernel_internals/typing/ghost_cfg.ml 10 additions, 1 deletionsrc/kernel_internals/typing/ghost_cfg.ml
- src/kernel_internals/typing/oneret.ml 71 additions, 71 deletionssrc/kernel_internals/typing/oneret.ml
- src/kernel_internals/typing/oneret.mli 7 additions, 8 deletionssrc/kernel_internals/typing/oneret.mli
- src/kernel_services/ast_printing/cil_printer.ml 21 additions, 9 deletionssrc/kernel_services/ast_printing/cil_printer.ml
- src/kernel_services/ast_printing/printer_api.mli 7 additions, 5 deletionssrc/kernel_services/ast_printing/printer_api.mli
- src/kernel_services/ast_queries/cil.ml 33 additions, 24 deletionssrc/kernel_services/ast_queries/cil.ml
- src/kernel_services/ast_queries/cil.mli 19 additions, 7 deletionssrc/kernel_services/ast_queries/cil.mli
- src/plugins/e-acsl/src/code_generator/injector.ml 1 addition, 0 deletionssrc/plugins/e-acsl/src/code_generator/injector.ml
- src/plugins/e-acsl/tests/constructs/ghost.i 8 additions, 0 deletionssrc/plugins/e-acsl/tests/constructs/ghost.i
- src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c 6 additions, 0 deletionssrc/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
- tests/cil/ghost_cfg.c 26 additions, 0 deletionstests/cil/ghost_cfg.c
- tests/cil/oracle/ghost_cfg.0.res.oracle 6 additions, 0 deletionstests/cil/oracle/ghost_cfg.0.res.oracle
- tests/cil/oracle/ghost_cfg.1.res.oracle 1 addition, 1 deletiontests/cil/oracle/ghost_cfg.1.res.oracle
- tests/crowbar/test_ghost_cfg.ml 50 additions, 4 deletionstests/crowbar/test_ghost_cfg.ml
- tests/pretty_printing/ghost_else.i 39 additions, 0 deletionstests/pretty_printing/ghost_else.i
Loading
Please register or sign in to comment