K-user mailing list

[Traian Florin Şerbănuţă <traian.serbanuta AT fmi.unibuc.ro>]

Hi Imran,

Since it seems you want to execute both branches and to "join" their results, one suggestion would be two use a "stack" of memory frames, one for each nested conditional, where writes would only be done at the top level, while lookups would be done in the most recent frame containing the location being looked up. 

An idea which comes to my mind which makes sense in this setting would be to have a statement evaluate to the memory frame containing the assignments of the variables affected by that statement.

Then sequential composition would use the frame of the first statement as a base for the evaluation of the second.

Then if could be strict and then evaluate to the "join" of its branches.

best wishes,

Traian

On Thu, Jun 23, 2016 at 3:33 PM <imran.pcs16 AT iitp.ac.in> wrote:

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