false warning of "sub-expression cannot be evaluated"

[zhendongsu]

$ tis-interpreter.sh test1.c
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
test1.c:5:[value] warning: The following sub-expression cannot be evaluated:
                 a

                 All sub-expressions with their values:

                 Stopping
                 stack: main
[value] user error: Degeneration occurred:
                    results are not correct for lines of code that can be reached from the degeneration point.
$ 
$ tis-interpreter.sh test2.c
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] done for function main
$ 
$ cat test1.c
static volatile int a;

int main ()
{
  return a && 1; 
}
$ 
$ cat test2.c
static volatile int a;

int main ()
{
  return a;
}
$ 

[pascal-cuoq]

Neither example should be considered as a bug:

• the common use of volatile is to indicate that reading from a variable is an input. In order to run in tis-interpreter programs that receive inputs this way, some adjustment is necessary in order to let them receive their input in a different way. tis-interpreter tries to point out the closest program point it can to where a volatile variable is read.
• there is no guarantee that execution stops when a volatile variable is used, especially if it is used as expression in the return statement of the main function. This is fine because reading from a volatile variable is not a bug.

If you are using volatile only as a way to trigger compiler bugs and not to indicate extra inputs to the program, please use --cc -Dvolatile= in order to make tis-interpreter ignore it:

$ tis-interpreter.sh --cc -Dvolatile= test1.c
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] done for function main

[zhendongsu]

Thank you for the explanation, Pascal. I'll turn on --cc -Dvolatile=.

[regehr]

Defining away volatile is what I usually do when using tis-interpreter to detect UB.