Module Data_for_aorai

module Data_for_aorai: sig .. end
Module of data management used in all the plugin Aorai. Operations are mainly accessors for data. The use of this module is mainly done through the ltl_utils module.

Return the buchi automata as stored after parsing



Module of data management used in all the plugin Aorai. Operations are mainly accessors for data. The use of this module is mainly done through the ltl_utils module.
exception Empty_automaton
raised when simplifications make the resulting automaton empty, meaning that the code and the property do not match.

LTL/Promela primitives



LTL/Promela primitives



Here are some operations used for generation of LTL AST or Promela AST.
module Aorai_state: Datatype.S_with_collections  with type t = Promelaast.state
module Aorai_typed_trans: Datatype.S_with_collections  
  with 
    type t = (Promelaast.typed_condition * Promelaast.action) Promelaast.trans
val setCData : unit -> unit
Initializes some tables according to data from Cil AST.

Initializes some tables according to data from Cil AST.

val add_logic : string -> Cil_types.logic_info -> unit
val get_logic : string -> Cil_types.logic_info
val add_predicate : string -> Cil_types.logic_info -> unit
val get_predicate : string -> Cil_types.logic_info
val pebble_set_at : Cil_types.logic_info -> Cil_types.logic_label -> Cil_types.term
Given a logic info representing a set of pebbles and a label, returns the term corresponding to evaluating the set at the label.
val aux_variables : unit -> Cil_types.varinfo list
Global auxiliary variables generated during type-checking of transitions
val abstract_logic_info : unit -> Cil_types.logic_info list
Global logic info generated during type-checking (mostly encoding of ghost variables having a logic type)

Smart constructors for conditions