论文《基于懒替换的c符号执行》中的实验结果下载

《论文《基于懒替换的c符号执行》中的实验结果下载》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、Example1代码懒符号执行结果程序状态ijinti,j;@(I>5);j=4;@(i+j<8);@i>5j=4@i+4<8⊥⊥⊥⊥⊥⊥44Example2代码懒符号执行结果程序状态ijphp.valhp.nextstructmySt{intval;structmySt*next;};inti,*j;structmySt*p;{j=&i;*j=3;p=malloc(2);p->val=8;p->next=NULL;}j=&i;I=3;p=malloc(2);hp.val=8hp.next=NULL⊥⊥⊥⊥3333(⊥,⊥)

2、(⊥,⊥)(⊥,⊥)(i,⊥)(i,⊥)(i,⊥)(i,⊥)(i,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(hp,⊥)(hp,⊥)(hp,⊥)⊥88(⊥,⊥)(⊥,⊥)NULLExample4代码懒符号执行结果程序状态ijpinti,j;int*p;{scanf(“%d”,&i);scanf(“%d”,&j);@(i>2)&&(j>2);p=&i;*p=*p+j;@*p<2;}i=i0j=j0@i0>2&&j0>2p=&ii=i0+j0@i0+j0<2⊥⊥⊥i0i0i0i0i0+j0i0+j0⊥⊥⊥⊥j0j0j0j0j0

3、(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(i,⊥)(i,⊥)(i,⊥)Example3代码懒符号执行结果程序状态ijxxnrprrnlplhxn.datahxn.nexthx.datahx.nextstructnode{intdata;structnode*next;};inti,j;structnode*x,*xn,*r;structnode*pr,*rn,*l,*pl;{xn=malloc(2);xn->next=NULL;scanf("%d",&j);xn->data=j;x=malloc(2);x->nex

4、t=xn;scanf("%d",&i);x->data=i;//path@x!=NULLpr=x;r=x->next;xn=malloc(2)xn->next=NULLj=j0xn->data=j0x=malloc(2)x->next=xni=i0x->data=i0@x!=NULLpr=xr=x->next⊥⊥⊥⊥⊥⊥⊥⊥⊥i0i0i0i0i0⊥⊥⊥⊥⊥j0j0j0j0j0j0j0j0j0(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(h

5、x,⊥)(⊥,⊥)(⊥,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(hxn,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(hx,⊥)(hx,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)

6、(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)(⊥,⊥)⊥⊥⊥j0j0j0j0j0j0j0j0(⊥,⊥)NULLNULLNULLNULLNULLNULLNULLNULLNULLNULL⊥⊥⊥i0i0i0i0(⊥,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)@r!=NULL

7、pl=x;rn=r->next;l=x->next;@(l==r);pr=r;r=rn;@(r==NULL);//postcondition@(x->data>xn->data);}@r!=NULLpl=xrn=r->nextl=x->next@(l==r)pr=rr=rn@(r==NULL)@i0>j0i0i0i0i0i0i0i0i0i0j0j0j0j0j0j0j0j0j0(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(

8、hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥)NULLNULLNULL(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hx,⊥)(hxn,⊥)(hxn,⊥)(hxn,⊥