Merge branch 'feature/basile/eacsl-ensuresec-json' into 'master'
[eacsl] Add an example for the Ensuresec european project See merge request frama-c/frama-c!3474
No related branches found
No related tags found
Showing
- src/plugins/e-acsl/examples/ensuresec/.gitignore 1 addition, 0 deletionssrc/plugins/e-acsl/examples/ensuresec/.gitignore
- src/plugins/e-acsl/examples/ensuresec/Makefile 37 additions, 0 deletionssrc/plugins/e-acsl/examples/ensuresec/Makefile
- src/plugins/e-acsl/examples/ensuresec/README.md 38 additions, 0 deletionssrc/plugins/e-acsl/examples/ensuresec/README.md
- src/plugins/e-acsl/examples/ensuresec/ensuresec_ee.c 139 additions, 0 deletionssrc/plugins/e-acsl/examples/ensuresec/ensuresec_ee.c
- src/plugins/e-acsl/examples/ensuresec/json_assert.c 296 additions, 0 deletionssrc/plugins/e-acsl/examples/ensuresec/json_assert.c
- src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c 120 additions, 117 deletions...e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
- src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h 11 additions, 0 deletions...e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
- src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h 2 additions, 0 deletions...l/share/e-acsl/instrumentation_model/e_acsl_assert_data.h
- src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c 2 additions, 2 deletions...acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c
- src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c 3 additions, 2 deletions...e-acsl/observation_model/internals/e_acsl_heap_tracking.c
- src/plugins/e-acsl/src/code_generator/assert.ml 19 additions, 4 deletionssrc/plugins/e-acsl/src/code_generator/assert.ml
- src/plugins/e-acsl/src/code_generator/assert.mli 5 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/assert.mli
- src/plugins/e-acsl/tests/arith/oracle/gen_arith.c 2 additions, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_arith.c
- src/plugins/e-acsl/tests/arith/oracle/gen_array.c 36 additions, 18 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_array.c
- src/plugins/e-acsl/tests/arith/oracle/gen_at.c 8 additions, 4 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_at.c
- src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c 32 additions, 16 deletions...csl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
- src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c 24 additions, 12 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
- src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c 6 additions, 3 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
- src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c 18 additions, 9 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c 10 additions, 5 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
Loading
Please register or sign in to comment