package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file automaton_ast.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Aorai plug-in of Frama-C.                        *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*    INRIA (Institut National de Recherche en Informatique et en         *)
(*           Automatique)                                                 *)
(*    INSA  (Institut National des Sciences Appliquees)                   *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(** The abstract tree of Ya representation. Such tree is used by
    parser/lexer before its translation into Data_for_aorai module. *)

type expression =
  | PVar of string
  | PPrm of string * string (* f().N *)
  | PMetavar of string
  | PCst of Logic_ptree.constant
  | PBinop of Logic_ptree.binop * expression * expression
  | PUnop of Logic_ptree.unop * expression
  | PArrget of expression * expression
  | PField of expression * string
  | PArrow of expression * string

type condition =
  | PRel of Logic_ptree.relation * expression * expression
  | PTrue
  | PFalse
  | POr of condition * condition
  | PAnd of condition * condition
  | PNot of condition
  | PCall of string * string option
  (** Call might be done in a given behavior *)
  | PReturn of string

and seq_elt = {
  condition: condition option;
  nested: sequence;
  min_rep: expression option;
  max_rep: expression option;
}

and sequence = seq_elt list

(** Ya parsed abstract syntax trees. Either a sequence of event or the
    otherwise keyword. A single condition is expressed with a singleton
    having an empty nested sequence and min_rep and max_rep being equal to one.
*)
type guard = Seq of sequence | Otherwise

type action =
  | Metavar_assign of string * expression

type typed_condition =
  | TOr of typed_condition * typed_condition  (** Logical OR *)
  | TAnd of typed_condition * typed_condition (** Logical AND *)
  | TNot of typed_condition             (** Logical NOT *)
  | TCall of Cil_types.kernel_function * Cil_types.funbehavior option
  (** Predicate modelling the call of an operation *)
  | TReturn of Cil_types.kernel_function
  (** Predicate modelling the return of an operation *)
  | TTrue                         (** Logical constant TRUE *)
  | TFalse                        (** Logical constant FALSE *)
  | TRel of Cil_types.relation * Cil_types.term * Cil_types.term
  (** Condition. If one of the terms contains TResult, TRel is in
      conjunction with exactly one TReturn event, and the TResult is
      tied to the corresponding value.
  *)

(** Additional actions to perform when crossing a transition.
    There is at most one Pebble_* action for each transition, and
    each transition leading to a state with multi-state has such an action.
*)
type typed_action =
  | Counter_init of Cil_types.term_lval
  | Counter_incr of Cil_types.term_lval
  | Pebble_init of
      Cil_types.logic_info * Cil_types.logic_var * Cil_types.logic_var
  (** adds a new pebble. [Pebble_init(set,aux,count)] indicates that
      pebble [count] is put in [set] whose content is governed by C
      variable [aux].
  *)
  | Pebble_move of
      Cil_types.logic_info *
      Cil_types.logic_var * Cil_types.logic_info * Cil_types.logic_var
  (** [Pebble_move(new_set,new_aux,old_set,old_aux)]
      moves pebbles from [old_set] to [new_set], governed by the
      corresponding aux variables. *)
  | Copy_value of Cil_types.term_lval * Cil_types.term
  (** copy the current value of the given term into the given location
      so that it can be accessed by a later state. *)


(** Internal representation of a State from the Buchi automata. *)
type state = {
  name : string;                 (** State name *)
  mutable acceptation : Bool3.t; (** True iff state is an acceptation state *)
  mutable init : Bool3.t;        (** True iff state is an initial state *)
  mutable nums : int;            (** Numerical ID of the state *)
  mutable multi_state: (Cil_types.logic_info * Cil_types.logic_var) option;
  (** Translation of some sequences might lead to some kind of pebble
      automaton, where we need to distinguish various branches. This is
      done by having a set of pebbles instead of just a zero/one switch
      to know if we are in the given state. The guards apply to each
      active pebble and are thus of the form
      \forall integer x; in(x,multi_state) ==> guard.
      multi_state is the first lvar of the pair, x is the second
  *)
}

(** Internal representation of a transition from the Buchi automata. *)
type ('c,'a) trans = {
  start : state ;            (** Starting state of the transition *)
  stop : state ;             (** Ending state of the transition *)
  mutable cross : 'c;        (** Cross condition of the transition *)
  mutable actions : 'a list; (** Actions to execute while crossing *)
  mutable numt : int         (** Numerical ID of the transition *)
}

type ('c,'a) graph = state list * ('c, 'a) trans list

type parsed_trans = (guard, action) trans

type typed_trans = (typed_condition, typed_action) trans

(** Internal representation of a Buchi automata : a list of states and a list
    of transitions.*)
type ('c,'a) automaton = {
  states: state list;
  trans: ('c,'a) trans list;
  metavariables: Cil_types.varinfo Datatype.String.Map.t;
  observables: Datatype.String.Set.t option;
}

type parsed_automaton = (guard, action) automaton

type typed_automaton = (typed_condition, typed_action) automaton

(** An operation can have two status: currently calling or returning. *)
type funcStatus =
  | Call
  | Return

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct