Skip to content
Snippets Groups Projects
Commit 0dc96aa6 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

[tests] Improved test case initialized to cover a bug in partial

initialization [ see 61afda4f1ba39f2b9ec5dff3c5cb118402457031 ]
parent 765633c9
No related branches found
No related tags found
No related merge requests found
......@@ -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); */
}
......@@ -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));
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment