TYPE PSign = set(snum) PSignLifted = lift(PSign) State = Var -> PSignLifted PROBLEM OwnAnalysis direction : forward carrier : State init : bot init_start : [-> top] combine : nLUB TRANSFER // in assignments calculate the new value of the variable and add it to the state ASSIGN(variable, expression) = if @ = bot then bot else @\[variable -> evalAExp(expression,@)] endif // test conditions IF(expression), true_edge = branch(expression,@,true) IF(expression), false_edge = branch(expression,@,false) // loop conditions WHILE(expression), true_edge = branch(expression,@,true) WHILE(expression), false_edge = branch(expression,@,false) SUPPORT negZ :: -> PSign negZ() = {-1,-2} posZ :: -> PSign posZ() = {1,2} signs :: PSign -> PSign //signs(s) returns a set that contains -1,-2 if s contains a negative number, 1,2 if s contains a positive number, and 0 if s contains 0 signs(s) = {a | b in {if (x>0) then posZ() else if (x=0) then {0} else negZ() endif endif | x in s}; a in b} singleton :: PSign -> bool //returns true if s contains at most one element singleton(s) = !({1 |x1 in s; x2 in s; x1!=x2}={1}) nLUB :: State*State->State nLUB(e1,e2) = [ [->top]\(a,c) |(a,b) in (e1 lub e2)\top; b!=bot; let c=(if e1=(e1 lub e2) then b else ( if signs(drop(b))=negZ() then lift(negZ()) else if signs(drop(b))=posZ() then lift(posZ()) else top endif endif ) endif)] evalAExp :: Expression * State -> PSignLifted evalAExp(expression, state) = case expType(expression) of "ARITH_BINARY" => case expOp(expression) of "+" => let valLeft <= evalAExp(expSubLeft(expression),state), valRight <= evalAExp(expSubRight(expression),state) in if (singleton(valLeft) && singleton(valRight)) then lift({x+y|x in valLeft; y in valRight}) else if (signs(valLeft)=signs(valRight)) then lift(signs(valLeft)) else top endif endif; "-" => let valLeft <= evalAExp(expSubLeft(expression),state), valRight <= evalAExp(expSubRight(expression),state) in if (singleton(valLeft) && singleton(valRight)) then lift({x-y|x in valLeft; y in valRight}) else top endif; "*" => let valLeft = evalAExp(expSubLeft(expression), state), valRight = evalAExp(expSubRight(expression),state) in if (valLeft=lift({0}) || valRight=lift({0})) then lift({0}) else if (valLeft=bot || valRight = bot) then bot else if (valLeft=top && valRight=top) then top else if (singleton(drop(valLeft)) && singleton(drop(valRight))) then lift({x*y|x in drop(valLeft); y in drop(valRight)}) else top endif endif endif endif; "/" => let valLeft <= evalAExp(expSubLeft(expression),state), valRight <= evalAExp(expSubRight(expression),state) in if (valRight={0}) then bot else top endif; endcase; "ARITH_UNARY" => case expOp(expression) of "-" => let value <= evalAExp(expSub(expression), state) in lift({-x | x in value}); endcase; "VAR" => state ( expVar(expression) ); "CONST" => lift({expVal(expression)}); _ => error("Runtime Error: evalAExp applied to nonarithmetic Expression"); endcase branch :: Expression * State * bool -> State branch(expression, state, edge) = state