[e-acsl] compile logic functions if they're evoked with the Here label
This commit adds a Here inliner to Logic_normalizer, which specialises labelled logic functions that are called somewhere exclusively with Here labels.
Showing
- src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/src/analyses/logic_normalizer.ml 177 additions, 2 deletionssrc/plugins/e-acsl/src/analyses/logic_normalizer.ml
- src/plugins/e-acsl/src/analyses/logic_normalizer.mli 16 additions, 0 deletionssrc/plugins/e-acsl/src/analyses/logic_normalizer.mli
- 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 9 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/logic_functions.ml
- src/plugins/e-acsl/tests/arith/oracle/gen_functions.c 45 additions, 41 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 1 addition, 0 deletionssrc/plugins/e-acsl/tests/examples/functions_contiki.c
- src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle 5 additions, 5 deletions...e-acsl/tests/examples/oracle/functions_contiki.res.oracle
- src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c 53 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/libc/oracle/gen_mem.c 302 additions, 17 deletionssrc/plugins/e-acsl/tests/libc/oracle/gen_mem.c
- src/plugins/e-acsl/tests/libc/oracle/gen_str.c 30 additions, 26 deletionssrc/plugins/e-acsl/tests/libc/oracle/gen_str.c
- src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle 43 additions, 14 deletionssrc/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
- src/plugins/e-acsl/tests/libc/oracle/str.res.oracle 7 additions, 5 deletionssrc/plugins/e-acsl/tests/libc/oracle/str.res.oracle
- src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c 2 additions, 0 deletionssrc/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
Loading
Please register or sign in to comment