Download Paper - STS

Appendix
type predicate =
| Pfalse
| Ptrue
| Papp of logic info * (logic label *
logic label) list * term list
| Pseparated of term list
| Prel of relation * term * term
| Pand of predicate named * predicate
named
| Por of predicate named * predicate
named
| Pxor of predicate named * predicate
named
| Pimplies of predicate named * predicate
named
| Piff of predicate named * predicate
named
| Pnot of predicate named
| Pif of term * predicate named * predicate named
| Plet of logic info * predicate named
| Pforall of quantifiers * predicate named
| Pexists of quantifiers * predicate named
| Pat of predicate named * logic label
| Pvalid read of logic label * term
| Pvalid of logic label * term
| Pinitialized of logic label * term
| Pallocable of logic label * term
| Pfreeable of logic label * term
| Pfresh of logic label * logic label * term
* term
| Psubtype of term * term
(* always-false predicate. *)
(* always-true predicate. *)
(* application of a predicate. *)
(* comparison of two terms. *)
(* conjunction *)
(* disjunction. *)
(* logical xor. *)
(* implication. *)
(* equivalence. *)
(* negation. *)
(* conditional *)
(* definition of a local variable *)
(* universal quantification. *)
(* existential quantification. *)
(* predicate refers to a particular program point. *)
(* the given locations are valid for reading. *)
(* the given locations are valid. *)
(* the given locations are initialized. *)
(* the given locations can be allocated. *)
(* the given locations can be free. *)
(* \fresh(pointer, n) A memory block of n bytes is
newly allocated to the pointer. *)
(* First term is a type tag that is a subtype of the
second. *)
Table 1: Predicates of Frama-C
75