Commit 027b0d44 authored by Julien Signoles's avatar Julien Signoles

[e-acsl] Michele's review

parent 81eaf1a1
......@@ -30,7 +30,7 @@ open Cil_types
exception Unregistered_library_function of string
val get_lib_fun_vi: string -> varinfo
(** Return varinfo corresponding to a name of a given library function *)
(** @return varinfo corresponding to a name of a given library function *)
(* ************************************************************************** *)
(** {2 Handling \result} *)
......@@ -80,14 +80,14 @@ val is_set_of_ptr_or_array: logic_type -> bool
(** Checks whether the given logic type is a set of pointers. *)
val is_range_free: term -> bool
(** Returns [true] iff the given term does not contain any range. *)
(** @return true iff the given term does not contain any range. *)
val is_bitfield_pointers: logic_type -> bool
(** Returns [true] iff the given logic type is a bitfield pointer or a
(** @return true iff the given logic type is a bitfield pointer or a
set of bitfield pointers. *)
val term_has_lv_from_vi: term -> bool
(** Return [true] iff the given term contains a variables that originates from
(** @return true iff the given term contains a variables that originates from
a C varinfo, that is a non-purely logic variable. *)
type pred_or_term = PoT_pred of predicate | PoT_term of term
......@@ -97,13 +97,13 @@ val mk_ptr_sizeof: typ -> location -> exp
to a [typ] typ and returns [sizeof(typ)]. *)
val name_of_binop: binop -> string
(** Returns the name of the given binop as a string *)
(** @return the name of the given binop as a string. *)
val finite_min_and_max: Ival.t -> Integer.t * Integer.t
(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)
(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds. *)
module Id_term: Datatype.S_with_collections with type t = term
(** datatype for terms that relies on physical equality *)
(** Datatype for terms that relies on physical equality. *)
(*
Local Variables:
......
......@@ -30,8 +30,9 @@ let dkey = Options.dkey_prepare
let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
(* The purpose of [actions] is similar to the Frama-C visitor's [actions] but we
need to fill it outside the visitor. So it is our own version. *)
(* The purpose of [actions] is similar to the Frama-C visitor's
[get_filling_actions] but we need to fill it outside the visitor. So it is
our own version. *)
let actions = Queue.create ()
(* global table for ensuring that logic info are not shared between a function
......@@ -211,7 +212,6 @@ let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
Globals.Functions.register kf
end)
actions;
Options.feedback ~dkey ~level:2 "function %s" name;
(* remove the specs attached to the previous kf iff it is a definition:
it is necessary to keep stable the number of annotations in order to get
[Keep_status] working fine. *)
......@@ -262,7 +262,7 @@ let sufficiently_aligned vi algn =
if acc <> 0 && acc <> alignment then begin
(* multiple align attributes with different values *)
Options.error
"multiple alignment attributs with different values for\
"multiple alignment attributes with different values for\
variable %a. Keeping the last one."
Printer.pp_varinfo vi;
alignment
......
Markdown is supported
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