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 (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Logic_parser/index.html

Module `Frama_c_kernel.Logic_parser`

type token =

| WSTRING_CONSTANT of string
| WRITES
| WITH
| VOLATILE
| VOID
| VARIANT
| VALID_READ
| VALID_RANGE
| VALID_INDEX
| VALID_FUNCTION
| VALID
| UNSIGNED
| UNION
| UNALLOCATED
| TYPEOF
| TYPENAME of string
| TYPE
| TRUE
| TILDE
| TERMINATES
| STRUCT
| STRING_LITERAL of bool * string
| STRING_CONSTANT of string
| STATIC
| STARHAT
| STAR
| SLICE
| SLASH
| SIZEOF
| SIGNED
| SHORT
| SEPARATED
| SEMICOLON
| RSQUAREPIPE
| RSQUARE
| RPAR
| RETURNS
| RESULT
| REQUIRES
| REGISTER
| REAL
| READS
| RBRACE
| QUESTION
| PREDICATE
| PRAGMA
| PLUS
| PIPE
| PI
| PERCENT
| OR
| OLD
| OFFSET
| OBJECT_POINTER
| NULL
| NOTHING
| NOT
| NE
| MODULE
| MODEL
| MINUS
| LTLT
| LT
| LSQUAREPIPE
| LSQUARE
| LPAR
| LOOP
| LONG
| LOGIC
| LET
| LEMMA
| LE
| LBRACE
| LAMBDA
| LABEL
| INVARIANT
| INT_CONSTANT of string
| INTER
| INTEGER
| INT
| INITIALIZED
| INDUCTIVE
| INCLUDE
| IN
| IMPLIES
| IMPACT
| IFF
| IF
| IDENTIFIER of string
| HATHAT
| HAT
| GTGT
| GT
| GLOBAL
| GHOST
| GE
| FUNCTION
| FROM
| FRESH
| FREES
| FREEABLE
| FORALL
| FOR
| FLOAT_CONSTANT of string
| FLOAT
| FALSE
| EXT_LET
| EXT_GLOBAL_BLOCK of string
| EXT_GLOBAL of string
| EXT_CONTRACT of string
| EXT_CODE_ANNOT of string
| EXT_AT
| EXITS
| EXISTS
| EQUAL
| EQ
| EOF
| ENUM
| ENSURES
| EMPTY
| ELSE
| DYNAMIC
| DOUBLE
| DOTDOTDOT
| DOTDOT
| DOT
| DOLLAR
| DISJOINT
| DECREASES
| DANGLING
| CONTRACT
| CONTINUES
| CONST
| COMPLETE
| COMMA
| COLONCOLON
| COLON2
| COLON
| CHECK_RETURNS
| CHECK_REQUIRES
| CHECK_LOOP
| CHECK_LEMMA
| CHECK_INVARIANT
| CHECK_EXITS
| CHECK_ENSURES
| CHECK_CONTINUES
| CHECK_BREAKS
| CHECK
| CHAR
| CASE
| BSUNION
| BSTYPE
| BSGHOST
| BREAKS
| BOOLEAN
| BOOL
| BLOCK_LENGTH
| BIMPLIES
| BIFF
| BEHAVIORS
| BEHAVIOR
| BASE_ADDR
| AXIOMATIC
| AXIOM
| AUTOMATIC
| AT
| ASSUMES
| ASSIGNS
| ASSERT
| ARROW
| AND
| AMP
| ALLOCATION
| ALLOCATES
| ALLOCABLE
| ADMIT_RETURNS
| ADMIT_REQUIRES
| ADMIT_LOOP
| ADMIT_LEMMA
| ADMIT_INVARIANT
| ADMIT_EXITS
| ADMIT_ENSURES
| ADMIT_CONTINUES
| ADMIT_BREAKS
| ADMIT

exception Error

val spec : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Logic_ptree.spec

val lexpr_eof : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Logic_ptree.lexpr

val ext_spec : 
  (Lexing.lexbuf -> token) ->
  Lexing.lexbuf ->
  Logic_ptree.ext_spec

val annot : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Logic_ptree.annot