[Kernel] New assertion kind: Assert or Check.
Asserts are both evaluated and used as hypotheses afterwards. Checks are only evaluated, but are not used as hypotheses: they must not affect the analyses.
Showing
- src/kernel_internals/parsing/logic_lexer.mll 1 addition, 0 deletionssrc/kernel_internals/parsing/logic_lexer.mll
- src/kernel_internals/parsing/logic_parser.mly 6 additions, 2 deletionssrc/kernel_internals/parsing/logic_parser.mly
- src/kernel_internals/typing/cabs2cil.ml 2 additions, 2 deletionssrc/kernel_internals/typing/cabs2cil.ml
- src/kernel_internals/typing/cfg.ml 6 additions, 2 deletionssrc/kernel_internals/typing/cfg.ml
- src/kernel_internals/typing/oneret.ml 1 addition, 1 deletionsrc/kernel_internals/typing/oneret.ml
- src/kernel_services/analysis/interpreted_automata.ml 3 additions, 2 deletionssrc/kernel_services/analysis/interpreted_automata.ml
- src/kernel_services/analysis/logic_interp.ml 1 addition, 1 deletionsrc/kernel_services/analysis/logic_interp.ml
- src/kernel_services/ast_data/alarms.ml 1 addition, 1 deletionsrc/kernel_services/ast_data/alarms.ml
- src/kernel_services/ast_data/annotations.ml 7 additions, 3 deletionssrc/kernel_services/ast_data/annotations.ml
- src/kernel_services/ast_data/annotations.mli 6 additions, 0 deletionssrc/kernel_services/ast_data/annotations.mli
- src/kernel_services/ast_data/cil_types.mli 7 additions, 1 deletionsrc/kernel_services/ast_data/cil_types.mli
- src/kernel_services/ast_data/property.ml 7 additions, 4 deletionssrc/kernel_services/ast_data/property.ml
- src/kernel_services/ast_printing/cil_printer.ml 6 additions, 1 deletionsrc/kernel_services/ast_printing/cil_printer.ml
- src/kernel_services/ast_printing/cil_types_debug.ml 6 additions, 2 deletionssrc/kernel_services/ast_printing/cil_types_debug.ml
- src/kernel_services/ast_printing/description.ml 15 additions, 5 deletionssrc/kernel_services/ast_printing/description.ml
- src/kernel_services/ast_printing/logic_print.ml 7 additions, 2 deletionssrc/kernel_services/ast_printing/logic_print.ml
- src/kernel_services/ast_queries/cil.ml 2 additions, 2 deletionssrc/kernel_services/ast_queries/cil.ml
- src/kernel_services/ast_queries/cil_datatype.ml 1 addition, 1 deletionsrc/kernel_services/ast_queries/cil_datatype.ml
- src/kernel_services/ast_queries/filecheck.ml 1 addition, 1 deletionsrc/kernel_services/ast_queries/filecheck.ml
- src/kernel_services/ast_queries/logic_typing.ml 5 additions, 2 deletionssrc/kernel_services/ast_queries/logic_typing.ml
Loading
Please register or sign in to comment