Ensure we are using volatile correctly

[adpaco-aws]

According to @danielsn:

volatile has two meanings: one is just that we can't reorder or drop the access, which CBMC never does.
It might also mean that reads should return nondet, which we don't currently model.

The code for this would be in intrinsics.rs

[adpaco-aws]

(Adding comment as part of #727)

Because concurrency is out of scope, volatile instructions should be treated as sequential operations. We should issue a warning when code is generated for them, similar to how we handle atomic intrinsics.

[adpaco-aws]

Closing this because now it's clear what is the right meaning for volatile in Kani: Since concurrency is out of scope for now, volatile operations should be treated as their non-volatile counterparts, and as indicated in the original description for the issue reordering is not an issue with CBMC. Note this already being done at least for intrinsics after the general audit in #727, which disabled all volatile intrinsics except for volatile_store.

If we were to tackle concurrency at some point in the future, then volatile operations should be reviewed to ensure proper handling. In my experience, treating volatile reads as nondet (I think there was such an option in CBMC) is certainly going to cause spurious failures in the long run, especially because it's not possible to automatically constrain the values that are being read.