Merge branch 'feature/basile/92-eacsl-behaviors' into 'master'
[eacsl] Support of active, complete and disjoint behaviors. Closes e-acsl#27 and e-acsl#92 See merge request frama-c/frama-c!2607
Showing
- src/kernel_services/ast_data/property.ml 19 additions, 11 deletionssrc/kernel_services/ast_data/property.ml
- src/kernel_services/ast_data/property.mli 1 addition, 1 deletionsrc/kernel_services/ast_data/property.mli
- src/kernel_services/ast_printing/description.ml 13 additions, 6 deletionssrc/kernel_services/ast_printing/description.ml
- src/plugins/e-acsl/.gitignore 1 addition, 0 deletionssrc/plugins/e-acsl/.gitignore
- src/plugins/e-acsl/E_ACSL.mli 13 additions, 5 deletionssrc/plugins/e-acsl/E_ACSL.mli
- src/plugins/e-acsl/Makefile.in 58 additions, 2 deletionssrc/plugins/e-acsl/Makefile.in
- src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/doc/refman/changes_modern.tex 2 additions, 0 deletionssrc/plugins/e-acsl/doc/refman/changes_modern.tex
- src/plugins/e-acsl/doc/refman/fn_behavior.tex 3 additions, 3 deletionssrc/plugins/e-acsl/doc/refman/fn_behavior.tex
- src/plugins/e-acsl/doc/refman/intro_modern.tex 1 addition, 2 deletionssrc/plugins/e-acsl/doc/refman/intro_modern.tex
- src/plugins/e-acsl/examples/contracts/function_contract.c 42 additions, 0 deletionssrc/plugins/e-acsl/examples/contracts/function_contract.c
- src/plugins/e-acsl/examples/contracts/statement_contract.c 42 additions, 0 deletionssrc/plugins/e-acsl/examples/contracts/statement_contract.c
- src/plugins/e-acsl/headers/header_spec.txt 10 additions, 0 deletionssrc/plugins/e-acsl/headers/header_spec.txt
- src/plugins/e-acsl/share/e-acsl/e_acsl.h 1 addition, 0 deletionssrc/plugins/e-acsl/share/e-acsl/e_acsl.h
- src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c 1 addition, 0 deletionssrc/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
- src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c 158 additions, 0 deletions...acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c
- src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h 124 additions, 0 deletions...acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h
- src/plugins/e-acsl/src/analyses/exit_points.mli 2 additions, 2 deletionssrc/plugins/e-acsl/src/analyses/exit_points.mli
- src/plugins/e-acsl/src/code_generator/contract.ml 753 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/contract.ml
- src/plugins/e-acsl/src/code_generator/contract.mli 47 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/contract.mli
Loading
Please register or sign in to comment