Module `Gil_syntax`

module Location : sig ... end

Representation of a location in a source file

module LVar : sig ... end

Allocator for logical variable names

module ALoc : sig ... end

Allocator for (sybolic) memory locations

module Var : sig ... end

GIL Variables

module Constant : sig ... end

GIL Constants

module Type : sig ... end

GIL Types

module Literal : sig ... end

GIL Literals

module UnOp : sig ... end

GIL Unary Operators

module BinOp : sig ... end

GIL Binary Operators

module NOp : sig ... end

GIL N-ary Operators

module Expr : sig ... end

GIL Expressions

module Formula : sig ... end

GIL Formulae

module Asrt : sig ... end

GIL Assertions

module SLCmd : sig ... end

GIL Separation-Logic Commands

module LCmd : sig ... end

GIL Logical Commands

module Cmd : sig ... end

GIL Commands

module Pred : sig ... end

GIL Predicates

module Lemma : sig ... end

GIL Lemmas

module Macro : sig ... end

GIL Macros

module Flag : sig ... end

Return-flags for GIL specifications

module Spec : sig ... end

GIL specifications

module BiSpec : sig ... end

Bi-abductive specifications

module Branch_case : sig ... end

Reasons for a branch in execution.

module Annot : sig ... end

Annotations for GIL commands

module Proc : sig ... end

Labeled GIL procedures

module Prog : sig ... end

A full GIL program

module Visitors : sig ... end

Classes for traversing the GIL AST