package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/qed/Qed/Engine/index.html

Module `Qed.Engine`Source

Generic Engine Signature

Sourcetype op =

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

Sourcetype 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
*)

Sourcetype 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 ...
*)

Sourcetype 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.
*)

Sourcetype flow =

| Flow
| Atom

Sourcetype cmode =

| Cprop
| Cterm

Sourcetype amode =

| Aint
| Areal

Sourcetype pmode =

| Positive
| Negative
| Boolean

Sourcetype ('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

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

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

Sourcetype scope = [

| `Auto
| `Unfolded
| `Defined of string

]

Sourcemodule type Env = sig ... end