[eacsl] Fix global C variable __e_acsl_sound_verdict
- The global variable is now a Frama-C built-in and is not monitored; - The `varinfo` for the variable, retrieved in module `Prepare_ast` is now exposed; - The variable is added to every generated code so that it can be used by a later analysis of E-ACSL.
Showing
- src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h 1 addition, 1 deletion...e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
- src/plugins/e-acsl/src/project_initializer/prepare_ast.ml 8 additions, 8 deletionssrc/plugins/e-acsl/src/project_initializer/prepare_ast.ml
- src/plugins/e-acsl/src/project_initializer/prepare_ast.mli 7 additions, 0 deletionssrc/plugins/e-acsl/src/project_initializer/prepare_ast.mli
- src/plugins/e-acsl/tests/arith/oracle/gen_arith.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_arith.c
- src/plugins/e-acsl/tests/arith/oracle/gen_array.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_array.c
- src/plugins/e-acsl/tests/arith/oracle/gen_at.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_at.c
- src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c 1 addition, 1 deletion...csl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
- src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
- src/plugins/e-acsl/tests/arith/oracle/gen_cast.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_cast.c
- src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
- src/plugins/e-acsl/tests/arith/oracle/gen_functions.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_functions.c
- src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
- src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
- src/plugins/e-acsl/tests/arith/oracle/gen_let.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_let.c
- src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
- src/plugins/e-acsl/tests/arith/oracle/gen_not.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_not.c
- src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
- src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
- src/plugins/e-acsl/tests/arith/oracle/gen_sum.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_sum.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
Loading
Please register or sign in to comment