cprover
|
This document describes the options available in goto-instrument for modelling the behaviour of volatile variables. The following options are provided:
--nondet-volatile
--nondet-volatile-variable <variable>
--nondet-volatile-model <variable>:<model>
By default, cbmc treats volatile variables the same as non-volatile variables. That is, it assumes that a volatile variable does not change between subsequent reads, unless it was written to by the program. With the above options, goto-instrument can be instructed to instrument the given goto program such as to (1) make reads from all volatile expressions non-deterministic (--nondet-volatile
), (2) make reads from specific variables non-deterministic (--nondet-volatile-variable
), or (3) model reads from specific variables by given models (--nondet-volatile-model
).
Below we give two usage examples for the options. Consider the following test, for function get_celsius()
and with harness test_get_celsius()
:
Here the variable temperature
corresponds to a hardware sensor. It returns the current temperature on each read. The get_celsius()
function converts the value in Kelvin to degrees Celsius, given the value is in the expected range. However, it has a bug where it reads temperature
a second time after the check, which may yield a value for which the check would not succeed. Verifying this program as is with cbmc would yield a verification success. We can use goto-instrument to make reads from temperature
non-deterministic:
Here the final invocation of cbmc correctly reports a verification failure.
However, simply treating volatile variables as non-deterministic may for some use cases be too inaccurate. Consider the following test, for function get_message()
and with harness test_get_message()
:
The harness verifies that get_message()
assigns non-decreasing timestamps to the returned messages. However, simply treating clock
as non-deterministic would not allow to prove this property. Thus, we can supply a model for reads from clock
:
The model is stateful in that it keeps the current clock value between invocations in the variable clock_value
. On each invocation, it increments the clock by a non-determinstic value in the range 0 to 100. We can tell goto-instrument to use the model clock_read_model()
for reads from the variable clock
as follows:
Now the final invocation of cbmc reports verification success.