The compiler performs a number of inferences, based on program text. They are meant to reduce annotation clutter, but can be always disabled using:

vcc_attr("no_infer", "inference-name")


For example vcc_attr("no_infer", "in_domain") . There is a special form: vcc_attr("no_infer", "all") , which will disable all the inferences.

Most of the inferences treat conjunctions of pre- or post-conditions as separate pre- or post-conditions.

The in_domain inference

For any object, for which wrapped(o) is unconditionally required in the preconditions, we put assert (in_domain(o ,o)); at the beginning of the function body.

The valid_claim inference

For any claim, for which wrapped(c) is unconditionally required in the preconditions, we put assert (valid_claim(c)); at the beginning of the function body.

The always_by_claim inference

For any claim c that is unconditionally required by the preconditions to unconditionally claim closed(o) , we insert always_by_claim(c, o) as a preconditions. Similarly for type invariants.

The by_claim inference

When always_by_claim(c, o) is present in the contract, replace all accesses to o->f , where f is a non-volatile field with by_claim(c, o->f) in the contract, as well as the body. In addition, inside the body look for assert(always_by_claim(c, o)); , and apply it till the end of the enclosing block. Similarly for type invariants.

The loop invariants

They are always inferred, regardless of flags.

If the loop body calls only pure functions and does not have an atomic block, we infer a free loop invariant that the type map and status map did not change.

If the loop body calls only functions with empty writes clauses we infer a free loop invariant that the set of mutable objects did not decrease.



Last edited Nov 13, 2009 at 12:03 PM by stobies, version 2

Comments

No comments yet.