Static Analysis
code step 1 : suppose we have code like this
int twic (int v) {
return 2*v;
}
void testme (int x int y) {
z= twic(y);
if (z==x) {
if(x>y+10) {
error}
}
}
Step 2 : Make a flow graph of the program
Step 3: Write them into mathematically form
after step 2 you have to write your diagram into math form like
suppose sign like your code
$(sigma type sign) : {x->xo y->yo} path condition Pc : true
if yes $ : {x->xo y->yo z->2*yo} (pc : true)^(2*yo=xo)
if false $ : {x->xo y->yo z->2*yo} (pc : true)^(2*yo!=xo)
Inner loop if True
$ : {x->xo y->yo z->2*yo} (pc : true)^(2*yo=xo)^xo>yo+10
Inner loop if False
$ : {x->xo y->yo z->2*yo} (pc : true)^(2*yo=xo)^xo<=yo+10
at the end valuse after solution
xo=2
yo=1
and hence .
Contact Me for any help
cheers !
