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.

exception Empty_automaton

raised when simplifications make the resulting automaton empty, meaning that the code and the property do not match.

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