That covers it really well @adityasharad !
It is worth noting that the getValue() predicate on Expr do get the compile time constant / folded expression value (if computed by Roslyn), but this is limited and will not cover the case presented in the example.

As a rule of thumb

• Roslyn (which is used by our extractor) folds expressions that are purely composed by compile time constants.
• Roslyn folds expressions where all operands are constants

That is, for the examples below the right hand side expressions are folded and will have a pre-computed constant value, which can be retrieved by Expr.getValue() except for string s4 = s1 + s2; (which is the most interesting case) as the operands are not constant.

const string c1 = "Hello";
const string c2 = "World";
const string c3 = "Hello" + "World";
const string c4 = c1 + c2;

string s1 = "Hello";
string s2 = "World";
string s3 = "Hello" + "World";
string s4 = s1 + s2;

As @adityasharad writes, we do not currently attempt to do any constant propagation in QL for C#, like we for example do for Ruby. In Ruby we would e.g. be able to infer that z has the value "ab" in

x = "a"
y = "b"
z = a + b

Thank you very much to @adityasharad for the response, and to @michaelnebel and @hvitved for the additional insights.
Is it possible to compute the set of possible values for a given variable? Here's an example:

string a = "a"; // line 1  
string b;  
if (1 == 1) {  
    b = "b"; // line 4  
} else if (1 != 1) {  
    b = "unreachable"; // line 6  
} else {  
    b = getNAC(); // line 8  
}  
string value = a + b; // line 10  
Console.WriteLine(value); // line 11  

My current approach is to use dfs and use-def chains. Assuming we have already modeled string concatenation, here is the manual analysis process:

1. The definition of value on line 11 comes from line 10.
2. The value on line 10 depends on the function call on the right-hand side. Since we have modeled string concatenation, we need to further analyze the strings being concatenated.
3. The value of variable a is defined at line 1, and it clearly has only one possible value: "a".
4. Variable b is defined in three places (lines 4, 6, and 8), so its possible values are "b" and "unreachable". Since we haven't modeled the getNAC function, we will ignore that value.
5. Finally, we take the Cartesian product of the possible values of a and b, so value could possibly be "ab" or "aunreachable".

It should in principle be doable, but I doubt it will be very useful in practice when expressions like getNAC() have unknown values.