Frama-C:
Plug-ins:
Libraries:

Frama-C API - Repr

High-Level Term Representation

Term & Predicate Introspection

type tau = Lang.F.tau
type var = Lang.F.var
type field = Lang.field
type lfun = Lang.lfun
type term = Lang.F.term
type pred = Lang.F.pred
type repr =
  1. | True
  2. | False
  3. | And of term list
  4. | Or of term list
  5. | Not of term
  6. | Imply of term list * term
  7. | If of term * term * term
  8. | Var of var
  9. | Int of Z.t
  10. | Real of Q.t
  11. | Add of term list
  12. | Mul of term list
  13. | Div of term * term
  14. | Mod of term * term
  15. | Eq of term * term
  16. | Neq of term * term
  17. | Lt of term * term
  18. | Leq of term * term
  19. | Times of Z.t * term
  20. | Call of lfun * term list
  21. | Field of term * field
  22. | Record of (field * term) list
  23. | Cst of tau * term
  24. | Get of term * term
  25. | Set of term * term * term
  26. | HigherOrder
    (*

    See Lang.F.e_open and Lang.F.e_close

    *)
val term : term -> repr
val pred : pred -> repr
val lfun : lfun -> string
val field : field -> string