X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2F4200-range-contains-2.html;fp=2020-frama-c%2F4200-range-contains-2.html;h=f64bb7e3e8837fe849fd4f44f41be3024a118f3c;hb=062da27127bc876eaeb4c728ed50bf744a3bcaa7;hp=0000000000000000000000000000000000000000;hpb=d8e14d47fcb1059c50c2af2652cb9837c70fc50f;p=libguestfs-talks.git diff --git a/2020-frama-c/4200-range-contains-2.html b/2020-frama-c/4200-range-contains-2.html new file mode 100644 index 0000000..f64bb7e --- /dev/null +++ b/2020-frama-c/4200-range-contains-2.html @@ -0,0 +1,24 @@ + + + + +
+ /*@ + predicate value_in_range(struct Range range, uint64_t value) = + range.lob <= value <= range.upb; + */ + + /* Does range contain val? */ + /*@ + requires \valid_read(range); + requires valid_range(*range); + assigns \nothing; + ensures \result <==> value_in_range(*range, val); + */ + static inline bool range_contains(const Range *range, uint64_t val) + { + return val >= range->lob && val <= range->upb; + } +