diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c index 88d367ba27053ca0861bcf21d5437fc4b101d711..c4c5edec1f4df1fd14de2c0ee6de870a86f31c79 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c @@ -116,4 +116,11 @@ int main(void) { /* @assert ! \initialized(partsc + i); */ } } + + /* Check duplicate initialization does not affect correct count of + * initialized bits (relevant for ADT models only). */ + int dup [2]; + dup[0] = 1; + dup[0] = 1; + /* @assert ! \initialized(&dup); */ } diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c index bfcf7fe7b539c001bb0ae6a5bc37226def804fab..e0be4e27e9ccd835e398e9470652c6ea849c940a 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c @@ -23,6 +23,7 @@ int main(void) int size; char *partsc; char *partsi; + int dup[2]; __e_acsl_memory_init((int *)0,(char ***)0,8UL); __e_acsl_globals_init(); __store_block((void *)(d),16UL); @@ -333,6 +334,8 @@ int main(void) i_0 ++; } } + dup[0] = 1; + dup[0] = 1; __retres = 0; __delete_block((void *)(& B)); __delete_block((void *)(& A));