Merge branch 'jan/eacsl-here-specialiser' into 'master'
[e-acsl] Here inliner: specialise logical functions called with the Here label See merge request frama-c/frama-c!4747
Showing
- src/kernel_services/ast_printing/cil_printer.ml 3 additions, 5 deletionssrc/kernel_services/ast_printing/cil_printer.ml
- src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/src/analyses/logic_normalizer.ml 220 additions, 36 deletionssrc/plugins/e-acsl/src/analyses/logic_normalizer.ml
- src/plugins/e-acsl/src/analyses/logic_normalizer.mli 22 additions, 0 deletionssrc/plugins/e-acsl/src/analyses/logic_normalizer.mli
- src/plugins/e-acsl/src/code_generator/assert.ml 5 additions, 1 deletionsrc/plugins/e-acsl/src/code_generator/assert.ml
- src/plugins/e-acsl/src/code_generator/assigns.ml 2 additions, 1 deletionsrc/plugins/e-acsl/src/code_generator/assigns.ml
- src/plugins/e-acsl/src/code_generator/logic_functions.ml 21 additions, 7 deletionssrc/plugins/e-acsl/src/code_generator/logic_functions.ml
- src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c 2 additions, 2 deletions...gins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
- src/plugins/e-acsl/tests/arith/oracle/gen_functions.c 45 additions, 38 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_functions.c
- src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle 5 additions, 2 deletionssrc/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
- src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c 125 additions, 123 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
- src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
- src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
- src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
- src/plugins/e-acsl/tests/examples/functions_contiki.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/examples/functions_contiki.c
- src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle 7 additions, 5 deletions...e-acsl/tests/examples/oracle/functions_contiki.res.oracle
- src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c 63 additions, 0 deletions...gins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
- src/plugins/e-acsl/tests/format/oracle/gen_printf.c 4 additions, 0 deletionssrc/plugins/e-acsl/tests/format/oracle/gen_printf.c
- src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c 1 addition, 1 deletion...s/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
- src/plugins/e-acsl/tests/libc/oracle/gen_mem.c 302 additions, 17 deletionssrc/plugins/e-acsl/tests/libc/oracle/gen_mem.c
Loading
Please register or sign in to comment