replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

assertions annotated 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3508 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2014-01-18 17:05:29 +00:00
parent 34fb7b0abc
commit 0eb7ca9d8c
1 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
regression/cbmc/Pointer_byte_extract5/main.c
View File

@ -13,21 +13,23 @@ typedef struct
} __attribute__((packed)) Struct3;
extern unsigned long __CPROVER_malloc_size;
int main() {
int main()
{
Struct3 *p = malloc (sizeof (int) + 2 * sizeof(Union));
p->Count = 3;
int po=0;
int m=__CPROVER_malloc_size;
p->List[0].a = 555;
__CPROVER_assert(p->List[0].b==555, "");
__CPROVER_assert(p->List[0].a==555, "");
__CPROVER_assert(p->List[0].b==555, "p->List[0].b==555");
__CPROVER_assert(p->List[0].a==555, "p->List[0].a==555");
// this should be fine
p->List[1].b = 999;
__CPROVER_assert(p->List[1].b==999, "");
__CPROVER_assert(p->List[1].a==999, "");
__CPROVER_assert(p->List[1].b==999, "p->List[1].b==999");
__CPROVER_assert(p->List[1].a==999, "p->List[1].a==999");
// this is out-of-bounds
p->List[2].a = 0;