X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2F4000-range-is-empty-again.html;fp=2020-frama-c%2F4000-range-is-empty-again.html;h=74e52f8e22cf47cd22bd0f77cdc89c0b34c04b16;hb=062da27127bc876eaeb4c728ed50bf744a3bcaa7;hp=0000000000000000000000000000000000000000;hpb=d8e14d47fcb1059c50c2af2652cb9837c70fc50f;p=libguestfs-talks.git diff --git a/2020-frama-c/4000-range-is-empty-again.html b/2020-frama-c/4000-range-is-empty-again.html new file mode 100644 index 0000000..74e52f8 --- /dev/null +++ b/2020-frama-c/4000-range-is-empty-again.html @@ -0,0 +1,30 @@ + + + + +
+ /*@ + predicate valid_range(struct Range range) = + range.lob <= range.upb + 1; + predicate empty_range(struct Range range) = + range.lob == range.upb + 1; + */ + + /* Is range empty? */ + /*@ + requires \valid_read(range); + requires valid_range(*range); + assigns \nothing; + ensures \result <==> empty_range(*range); + */ + static inline bool range_is_empty(const Range *range) + { + return range->lob > range->upb; + } ++ +
+ $ frama-c -wp -wp-rte snippets/range_is_empty.c +