K-user mailing list

[imran.pcs16 AT iitp.ac.in]

Hi, This is Imran from India. I am using K Framework for static
flow-sensitivity in Imperative language. Here every program variable and
constant initialized with 'low' and if a variable assigned with user input
then we mapped it to 'high' and if this variable used in any computation
with some other variable then other variable will be mapped to 'high'. For
example, Consider the following code:

int x,y;         // x,y initially mapped with 'low'
x= input(user);  // x mapped to high due to input from user
y=x;            // As x is mapped to high, y will be mapped to high.


I am unable to  to write rule for conditional statements like if-else.
Suppose a variable 'X' mapped to 'high' in if-part and 'low' to else-part.
After the execution of if-else statement ,variable should map to 'high' as
well as 'low'. If any further assignment of 'X'  comes after if-else 
statement, then 'X' mapping would remain same(i.e, X |-> (high,low) ). For
example, Consider the following code:

int x,y;
x = input(..);
if(...){
y = x;  // 'y' mapped to 'high' as 'x' is 'high'
}
else{
y = 10;    // y mapped to 'low'
}
-----
-----

Kindly suggest some rule to do the above task.



With Regards
Imran