Volatile intrinsics do not have to throw warnings

[adpaco-aws]

A volatile intrinsic implies the possibility of a concurrent access to memory, which Kani does not have support for. Therefore we should warn users that volatile instructions are treated sequentially.

[zhassan-aws]

Analysis: if the program creates threads, Kani will emit a warning/error when #922 is fixed.

If it doesn't create threads, then handling the volatile intrinsics in a sequential fashion is correct.

Based on this analysis, removing the "MLP - Must Have" label.

[zhassan-aws]

Ensuring we correctly handle them is captured in #58.

[adpaco-aws]

Renamed to "Volatile intrinsics do not have to throw warnings" (see @zhassan-aws above).