Commit 6ca4f146 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by Virgile Prevosto
Browse files

[Aorai] Remove three more files from the linter ignore list

parent de2147cc
......@@ -168,9 +168,6 @@ ML_LINT_KO+=src/plugins/aorai/logic_simplification.ml
ML_LINT_KO+=src/plugins/aorai/logic_simplification.mli
ML_LINT_KO+=src/plugins/aorai/ltl_output.ml
ML_LINT_KO+=src/plugins/aorai/path_analysis.ml
ML_LINT_KO+=src/plugins/aorai/promelaast.mli
ML_LINT_KO+=src/plugins/aorai/promelaoutput.ml
ML_LINT_KO+=src/plugins/aorai/promelaoutput.mli
ML_LINT_KO+=src/plugins/aorai/utils_parser.ml
ML_LINT_KO+=src/plugins/callgraph/callgraph_api.mli
ML_LINT_KO+=src/plugins/callgraph/cg.ml
......
......@@ -45,15 +45,15 @@ type condition =
| PAnd of condition * condition
| PNot of condition
| PCall of string * string option
(** Call might be done in a given behavior *)
(** 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 seq_elt = {
condition: condition option;
nested: sequence;
min_rep: expression option;
max_rep: expression option;
}
and sequence = seq_elt list
......@@ -63,82 +63,81 @@ and sequence = seq_elt list
*)
type guard = Seq of sequence | Otherwise
type action =
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.
*)
| 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].
*)
(** 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. *)
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
*)
}
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) 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 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.*)
(** 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;
......@@ -151,8 +150,8 @@ type typed_automaton = (typed_condition, typed_action) automaton
(** An operation can have two status: currently calling or returning. *)
type funcStatus =
| Call
| Return
| Call
| Return
(*
Local Variables:
......
......@@ -32,13 +32,13 @@ open Format
type 'a printer = Format.formatter -> 'a -> unit
let bool3_to_string = function
| True -> "True"
| False -> "False"
| Undefined -> "Undef"
let print_bool3 fmt b =
Format.pp_print_string fmt
(match b with
| True -> "True"
| False -> "False"
| Undefined -> "Undef")
Format.pp_print_string fmt (bool3_to_string b)
let print_state fmt st =
Format.fprintf fmt "@[<2>%s@ (acc=%a;@ init=%a;@ num=%d)@]"
......@@ -60,7 +60,7 @@ struct
| Ustar -> "*"
| Uamp -> "&"
| Ubw_not -> "~"
let rec print_expression fmt = function
| PVar s -> Format.fprintf fmt "%s" s
| PPrm (f,s) -> Format.fprintf fmt "%s().%s" f s
......@@ -73,11 +73,13 @@ struct
Format.fprintf fmt "(@[%a@])@ %a@ (@[%a@])"
print_expression e1 Printer.pp_binop (Logic_typing.type_binop bop)
print_expression e2
| PUnop(uop,e) -> Format.fprintf fmt "%s@;(@[%a@])"
(string_of_unop uop)
print_expression e
| PArrget(e1,e2) -> Format.fprintf fmt "%a@;[@(%a@]]"
print_expression e1 print_expression e2
| PUnop(uop,e) ->
Format.fprintf fmt "%s@;(@[%a@])"
(string_of_unop uop)
print_expression e
| PArrget(e1,e2) ->
Format.fprintf fmt "%a@;[@(%a@]]"
print_expression e1 print_expression e2
| PField(e,s) -> Format.fprintf fmt "%a.%s" print_expression e s
| PArrow(e,s) -> Format.fprintf fmt "%a->%s" print_expression e s
......@@ -89,12 +91,15 @@ struct
print_expression e2
| PTrue -> Format.pp_print_string fmt "true"
| PFalse -> Format.pp_print_string fmt "false"
| POr(e1,e2) -> Format.fprintf fmt "(@[%a@])@ or@ (@[%a@])"
print_condition e1 print_condition e2
| PAnd(e1,e2) -> Format.fprintf fmt "(@[%a@])@ and@ (@[%a@])"
print_condition e1 print_condition e2
| PNot c -> Format.fprintf fmt "not(@[%a@])"
print_condition c
| POr(e1,e2) ->
Format.fprintf fmt "(@[%a@])@ or@ (@[%a@])"
print_condition e1 print_condition e2
| PAnd(e1,e2) ->
Format.fprintf fmt "(@[%a@])@ and@ (@[%a@])"
print_condition e1 print_condition e2
| PNot c ->
Format.fprintf fmt "not(@[%a@])"
print_condition c
| PCall (s,None) -> Format.fprintf fmt "CALL(%s)" s
| PCall (s, Some b) -> Format.fprintf fmt "CALL(%s::%s)" s b
| PReturn s -> Format.fprintf fmt "RETURN(%s)" s
......@@ -107,7 +112,7 @@ struct
(Pretty_utils.pp_opt print_expression) elt.max_rep
and print_sequence fmt l =
Pretty_utils.pp_list ~pre:"[@[" ~sep:";@ " ~suf:"@]]" print_seq_elt fmt l
Pretty_utils.pp_list ~pre:"[@[" ~sep:";@ " ~suf:"@]]" print_seq_elt fmt l
let print_guard fmt = function
| Seq l -> print_sequence fmt l
......@@ -140,8 +145,10 @@ struct
print_condition c1 print_condition c2
| TNot c ->
Format.fprintf fmt "@[<hov 4>@[<hov 5>not(%a@])@]" print_condition c
| TTrue -> Format.pp_print_string fmt "True"
| TFalse -> Format.pp_print_string fmt "False"
| TTrue ->
Format.pp_print_string fmt "True"
| TFalse ->
Format.pp_print_string fmt "False"
| TRel(rel,exp1,exp2) ->
(* \result will be printed as such, not as f().return *)
Format.fprintf fmt "@[(%a)@]@ %a@ @[(%a)@]"
......@@ -258,10 +265,10 @@ struct
(Pretty_utils.pp_list dot_state) states
(Pretty_utils.pp_list dot_trans) trans
(fun fmt ->
if DotSeparatedLabels.get () then
(Format.fprintf fmt
"/* guards of transitions */@\ncomment=\"%a\";@\n"
(Pretty_utils.pp_list ~sep:"@\n" print_trans) trans));
if DotSeparatedLabels.get () then
(Format.fprintf fmt
"/* guards of transitions */@\ncomment=\"%a\";@\n"
(Pretty_utils.pp_list ~sep:"@\n" print_trans) trans));
Format.pp_set_formatter_out_functions fmt output_functions;
close_out cout
end
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment