[E-ACSL] fully fixed bug #1304 (1565534f) · Commits · pub / frama-c

Commit 1565534f authored 12 years ago by Julien Signoles

[E-ACSL] fully fixed bug #1304

[E-ACSL] fixed bug with array as argument of functions

parent 1a5ff2d0

No related branches found

No related tags found

Hide whitespace changes

Inline Side-by-side

Showing

src/plugins/e-acsl/misc.ml 7 additions, 4 deletions

src/plugins/e-acsl/misc.ml
src/plugins/e-acsl/pre_analysis.ml 38 additions, 13 deletions

src/plugins/e-acsl/pre_analysis.ml
src/plugins/e-acsl/tests/e-acsl-runtime/bts1304.i 27 additions, 0 deletions

src/plugins/e-acsl/tests/e-acsl-runtime/bts1304.i
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle 113 additions, 64 deletions

...ins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle 4 additions, 2 deletions

...ugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle 27 additions, 14 deletions

...lugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.err.oracle 0 additions, 0 deletions

...s/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.err.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle 257 additions, 0 deletions

...s/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.err.oracle 0 additions, 0 deletions

...ins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.err.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle 257 additions, 0 deletions

...ins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle 14 additions, 8 deletions

...gins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle 38 additions, 22 deletions

...-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle 78 additions, 39 deletions

...ests/e-acsl-runtime/oracle/function_contract.1.res.oracle
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c 113 additions, 64 deletions

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c 4 additions, 2 deletions

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c 27 additions, 14 deletions

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c 125 additions, 0 deletions

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c 125 additions, 0 deletions

...plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c 14 additions, 8 deletions

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c 38 additions, 22 deletions

...gins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c

with 1306 additions and 276 deletions

Please register or to comment