Simple Safety Query (State Reachability, Value Reachability, State and Value Reachability)

Supported Queries

State Reachability: Can the global state ever become state X? If we have no branching (etc: if statements), then this should be TRUE for all states. Otherwise the answer requires analysis.

Value Reachability: Can a variable M ever contain the value Z? If we never change the value for variable M, then we check if Z is the default value and return that value. Otherwise the answer requires analysis.

State and Value Reachability: A combination of the above: Can the global state ever become state X AND during state X is the variable M equal to the value Z? We need to reach the state X and have variable M store the value Z.

There are many more possible safety queries, but this is required to show a minimum viable product.

Query Format

/*!QUERY: <format>;*/