Frama-C API - `Engine`

Generic Engine Signature

type op =

| Op of string
(*
Infix or prefix operator
*)
| Assoc of string
(*
Left-associative binary operator (like + and -)
*)
| Call of string
(*
Logic function or predicate
*)

type link =

| F_call of string
(*
n-ary function
*)
| F_subst of string * string
(*
n-ary function with substitution first value is the link name, second is the substitution (e.g. "foo(%1,%2)")
*)
| F_left of string
(*
2-ary function left-to-right +
*)
| F_right of string
(*
2-ary function right-to-left +
*)
| F_list of string * string
(*
n-ary function with (cons,nil) constructors
*)
| F_assoc of string
(*
associative infix operator
*)
| F_bool_prop of string * string
(*
Has a bool and prop version
*)

type callstyle =

| CallVar
(*
Call is f(x,...) ; f() can be written f
*)
| CallVoid
(*
Call is f(x,...) ; in f(), () is mandatory
*)
| CallApply
(*
Call is f x ...
*)

type mode =

| Mpositive
(*
Current scope is Prop in positive position.
*)
| Mnegative
(*
Current scope is Prop in negative position.
*)
| Mterm
(*
Current scope is Term.
*)
| Mterm_int
(*
Int is required but actual scope is Term.
*)
| Mterm_real
(*
Real is required but actual scope is Term.
*)
| Mint
(*
Current scope is Int.
*)
| Mreal
(*
Current scope is Real.
*)

type flow =

| Flow
| Atom

type cmode =

| Cprop
| Cterm

type amode =

| Aint
| Areal

type pmode =

| Positive
| Negative
| Boolean

type ('x, 'f) ftrigger =

| TgAny
| TgVar of 'x
| TgGet of ('x, 'f) ftrigger * ('x, 'f) ftrigger
| TgSet of ('x, 'f) ftrigger * ('x, 'f) ftrigger * ('x, 'f) ftrigger
| TgFun of 'f * ('x, 'f) ftrigger list
| TgProp of 'f * ('x, 'f) ftrigger list

type ('t, 'f, 'c) ftypedef =

| Tabs
| Tdef of 't
| Trec of ('f * 't) list
| Tsum of ('c * 't list) list

type scope = [

| `Auto
| `Unfolded
| `Defined of string

]

module type Env = sig ... end

Generic Engine Signature

class type virtual ['z, 'adt, 'field, 'logic, 'tau, 'var, 'term, 'env] engine = object ... end