diff --git a/.Makefile.lint b/.Makefile.lint
index 0d06aec2a52cabd62013b44313fc1ec5de6f4143..5a4002feff4dae338f2f4e1b0ecce3417bb7c167 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -69,13 +69,10 @@ ML_LINT_KO+=src/kernel_services/ast_data/ast.mli
ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.ml
ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.mli
ML_LINT_KO+=src/kernel_services/ast_data/property_status.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.ml
-ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil_const.ml
ML_LINT_KO+=src/kernel_services/ast_queries/cil_const.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil_datatype.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil_state_builder.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/file.mli
ML_LINT_KO+=src/kernel_services/ast_queries/logic_const.mli
ML_LINT_KO+=src/kernel_services/ast_transformations/clone.ml
ML_LINT_KO+=src/kernel_services/ast_transformations/clone.mli
@@ -99,8 +96,6 @@ ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.ml
ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.mli
ML_LINT_KO+=src/kernel_services/visitors/cabsvisit.ml
ML_LINT_KO+=src/kernel_services/visitors/cabsvisit.mli
-ML_LINT_KO+=src/kernel_services/visitors/visitor.ml
-ML_LINT_KO+=src/kernel_services/visitors/visitor.mli
ML_LINT_KO+=src/libraries/datatype/datatype.ml
ML_LINT_KO+=src/libraries/datatype/datatype.mli
ML_LINT_KO+=src/libraries/datatype/descr.ml
@@ -189,7 +184,6 @@ ML_LINT_KO+=src/plugins/gui/analyses_manager.ml
ML_LINT_KO+=src/plugins/gui/book_manager.ml
ML_LINT_KO+=src/plugins/gui/book_manager.mli
ML_LINT_KO+=src/plugins/gui/design.mli
-ML_LINT_KO+=src/plugins/gui/filetree.mli
ML_LINT_KO+=src/plugins/gui/gtk_form.ml
ML_LINT_KO+=src/plugins/gui/gtk_form.mli
ML_LINT_KO+=src/plugins/gui/gui_printers.ml
@@ -233,8 +227,6 @@ ML_LINT_KO+=src/plugins/inout/register.ml
ML_LINT_KO+=src/plugins/loop_analysis/region_analysis.ml
ML_LINT_KO+=src/plugins/loop_analysis/region_analysis_stmt.ml
ML_LINT_KO+=src/plugins/metrics/metrics_acsl.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_base.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_base.mli
ML_LINT_KO+=src/plugins/metrics/metrics_cabs.ml
ML_LINT_KO+=src/plugins/metrics/metrics_cilast.mli
ML_LINT_KO+=src/plugins/metrics/metrics_coverage.ml
@@ -310,8 +302,6 @@ ML_LINT_KO+=src/plugins/studia/studia_gui.ml
ML_LINT_KO+=src/plugins/studia/studia_gui.mli
ML_LINT_KO+=src/plugins/users/users_register.ml
ML_LINT_KO+=src/plugins/value_types/cilE.mli
-ML_LINT_KO+=src/plugins/value_types/cvalue.ml
-ML_LINT_KO+=src/plugins/value_types/cvalue.mli
ML_LINT_KO+=src/plugins/value_types/function_Froms.ml
ML_LINT_KO+=src/plugins/value_types/function_Froms.mli
ML_LINT_KO+=src/plugins/value_types/inout_type.ml
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 5242bfbf931263cd07838ba48bb6512b112b532a..fb9a843d0a9db8be63c9b84b611fc86871564259 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -34,36 +34,36 @@ let is_integral_const = function
let rec possible_value_of_integral_const = function
| CInt64 (i,_,_) -> Some i
| CEnum {eival = e} -> possible_value_of_integral_expr e
- | CChr c -> Some (Integer.of_int (Char.code c))
+ | CChr c -> Some (Integer.of_int (Char.code c))
(* This is against the ISO C norm! See Cil.charConstToInt *)
| _ -> None
and possible_value_of_integral_expr e =
match (stripInfo e).enode with
- | Const c -> possible_value_of_integral_const c
- | _ -> None
+ | Const c -> possible_value_of_integral_const c
+ | _ -> None
let value_of_integral_const c =
match possible_value_of_integral_const c with
- | None -> assert false
- | Some i -> i
+ | None -> assert false
+ | Some i -> i
let value_of_integral_expr e =
match possible_value_of_integral_expr e with
- | None -> assert false
- | Some i -> i
+ | None -> assert false
+ | Some i -> i
let constant_expr ~loc i = new_exp ~loc (Const(CInt64(i,IInt,None)))
let rec is_null_expr e = match (stripInfo e).enode with
| Const c when is_integral_const c ->
- Integer.equal (value_of_integral_const c) Integer.zero
+ Integer.equal (value_of_integral_const c) Integer.zero
| CastE(_,e) -> is_null_expr e
| _ -> false
let rec is_non_null_expr e = match (stripInfo e).enode with
| Const c when is_integral_const c ->
- not (Integer.equal (value_of_integral_const c) Integer.zero)
+ not (Integer.equal (value_of_integral_const c) Integer.zero)
| CastE(_,e) -> is_non_null_expr e
| _ -> false
@@ -84,24 +84,24 @@ let possible_value_of_integral_logic_const = function
let value_of_integral_logic_const c =
match possible_value_of_integral_logic_const c with
- | None -> assert false
- | Some i -> i
+ | None -> assert false
+ | Some i -> i
let possible_value_of_integral_term t =
match t.term_node with
- | TConst c -> possible_value_of_integral_logic_const c
- | _ -> None
+ | TConst c -> possible_value_of_integral_logic_const c
+ | _ -> None
let term_lvals_of_term t =
let l = ref [] in
ignore
(Cil.visitCilTerm
(object
- inherit nopCilVisitor
- method! vterm_lval lv =
- l := lv :: !l;
- DoChildren
- end)
+ inherit nopCilVisitor
+ method! vterm_lval lv =
+ l := lv :: !l;
+ DoChildren
+ end)
t);
!l
@@ -119,8 +119,8 @@ let behavior_postcondition b k =
let behavior_precondition b =
let assumes = behavior_assumes b in
- let requires = Logic_const.pands
- (List.rev_map Logic_const.pred_of_id_pred b.b_requires)
+ let requires = Logic_const.pands
+ (List.rev_map Logic_const.pred_of_id_pred b.b_requires)
in
Logic_const.pimplies (assumes,requires)
@@ -134,16 +134,18 @@ let get_named_bhv bhv_list name =
let get_named_bhv_assumes spec bhv_names =
let bhvs = match bhv_names with
- | [] -> (* no names ==> all named behaviors *)
- List.filter (fun b -> not (is_default_behavior b)) spec.spec_behavior
- | _ ->
- let rec get l = match l with [] -> []
- | name::tl ->
- match get_named_bhv spec.spec_behavior name with
- | None -> (* TODO: warn ? *) get tl
- | Some b -> b::(get tl)
- in
- get bhv_names
+ | [] -> (* no names ==> all named behaviors *)
+ List.filter (fun b -> not (is_default_behavior b)) spec.spec_behavior
+ | _ ->
+ let rec get l =
+ match l with
+ | [] -> []
+ | name::tl ->
+ match get_named_bhv spec.spec_behavior name with
+ | None -> (* TODO: warn ? *) get tl
+ | Some b -> b::(get tl)
+ in
+ get bhv_names
in
List.map behavior_assumes bhvs
@@ -151,7 +153,7 @@ let complete_behaviors spec bhv_names =
let bhv_assumes = get_named_bhv_assumes spec bhv_names in
Logic_const.pors bhv_assumes
-let disjoint_behaviors spec bhv_names =
+let disjoint_behaviors spec bhv_names =
let bhv_assumes = get_named_bhv_assumes spec bhv_names in
let mk_disj_bhv b1 b2 = (* ~ (b1 /\ b2) *)
let p = Logic_const.pands [b1; b2] in
@@ -161,62 +163,64 @@ let disjoint_behaviors spec bhv_names =
let lp = List.map (mk_disj_bhv b) lb in
Logic_const.pands (prop::lp)
in
- let rec do_list prop l = match l with [] -> prop
- | b::tl ->
- let prop = do_one_with_list prop b tl in
- do_list prop tl
- in
- do_list Logic_const.ptrue bhv_assumes
+ let rec do_list prop l =
+ match l with
+ | [] -> prop
+ | b::tl ->
+ let prop = do_one_with_list prop b tl in
+ do_list prop tl
+ in
+ do_list Logic_const.ptrue bhv_assumes
let merge_assigns_internal (get:'b -> assigns) (origin:'b -> string list)
(acc:(('a*(bool * string list))*int) option) (bhvs: 'b list) =
- let cmp_assigns acc b =
+ let cmp_assigns acc b =
let a' = get b in
- match acc,a' with
- | _, WritesAny -> acc
- | None, Writes l ->
- (* use the number of assigned terms as measure *)
- Some ((a',(false,origin b)),List.length l)
- | (Some((a,(w,orig)),n)), Writes l ->
- let w = (* warning is needed? *)
- w || (a != a' && a <> WritesAny)
- in (* use the number of assigned terms as measure *)
- let m = List.length l in
- if n<0 || m<n then Some((a',(w,origin b)),m) else Some((a,(w,orig)),n)
+ match acc,a' with
+ | _, WritesAny -> acc
+ | None, Writes l ->
+ (* use the number of assigned terms as measure *)
+ Some ((a',(false,origin b)),List.length l)
+ | (Some((a,(w,orig)),n)), Writes l ->
+ let w = (* warning is needed? *)
+ w || (a != a' && a <> WritesAny)
+ in (* use the number of assigned terms as measure *)
+ let m = List.length l in
+ if n<0 || m<n then Some((a',(w,origin b)),m) else Some((a,(w,orig)),n)
in List.fold_left (* find the smallest one *)
- cmp_assigns acc bhvs
+ cmp_assigns acc bhvs
(** Returns the assigns from complete behaviors and unguarded behaviors. *)
let merge_assigns_from_complete_bhvs ?warn ?(unguarded=true) bhvs complete_bhvs =
let merge_assigns_from_complete_bhvs bhv_names =
try (* For merging assigns of a "complete" set of behaviors *)
let behaviors = match bhv_names with
- (* Extract behaviors from their names. *)
- | [] -> (* All behaviors should be taken except the default behavior *)
- List.filter (fun b -> not (Cil.is_default_behavior b)) bhvs
- | _ -> (* Finds the corresponding behaviors from the set *)
- List.map
- (fun b_name ->
- List.find (fun b -> b.b_name = b_name) bhvs) bhv_names
+ (* Extract behaviors from their names. *)
+ | [] -> (* All behaviors should be taken except the default behavior *)
+ List.filter (fun b -> not (Cil.is_default_behavior b)) bhvs
+ | _ -> (* Finds the corresponding behaviors from the set *)
+ List.map
+ (fun b_name ->
+ List.find (fun b -> b.b_name = b_name) bhvs) bhv_names
in
- (* Merges the assigns of the complete behaviors.
- Once one of them as no assumes, that means the merge
- of the unguarded behavior did already the job *)
+ (* Merges the assigns of the complete behaviors.
+ Once one of them as no assumes, that means the merge
+ of the unguarded behavior did already the job *)
Writes
- (List.fold_left
- (fun acc b -> match b.b_assigns with
- | Writes l when b.b_assumes <> [] -> l @ acc
- | _ -> raise Not_found) [] behaviors)
- with Not_found ->
+ (List.fold_left
+ (fun acc b -> match b.b_assigns with
+ | Writes l when b.b_assumes <> [] -> l @ acc
+ | _ -> raise Not_found) [] behaviors)
+ with Not_found ->
(* One of these behaviors is not found or has no assumes *)
WritesAny
in
let acc =
if unguarded then (* Looks first at unguarded behaviors. *)
- let unguarded_bhvs = List.filter (fun b -> b.b_assumes = []) bhvs
- in merge_assigns_internal (* Chooses the smallest one *)
- (fun b -> b.b_assigns) (fun b -> [b.b_name])
- None unguarded_bhvs
+ let unguarded_bhvs = List.filter (fun b -> b.b_assumes = []) bhvs
+ in merge_assigns_internal (* Chooses the smallest one *)
+ (fun b -> b.b_assigns) (fun b -> [b.b_name])
+ None unguarded_bhvs
else None
in
let acc = match acc with
@@ -226,28 +230,28 @@ let merge_assigns_from_complete_bhvs ?warn ?(unguarded=true) bhvs complete_bhvs
| _ ->
(* Look at complete behaviors *)
merge_assigns_internal (* Chooses the smallest one *)
- merge_assigns_from_complete_bhvs
- (fun bhvnames -> bhvnames)
- acc
- complete_bhvs
- in
+ merge_assigns_from_complete_bhvs
+ (fun bhvnames -> bhvnames)
+ acc
+ complete_bhvs
+ in
match acc with
| None -> WritesAny (* No unguarded behavior -> assigns everything *)
| Some ((a,(w,orig)),_) -> (* The smallest one *)
- let warn = match warn with
+ let warn = match warn with
| None -> w
- | Some warn -> warn
- in
+ | Some warn -> warn
+ in
if warn then begin
- let orig =
- if orig = [] then List.map (fun b -> b.b_name) bhvs else orig
+ let orig =
+ if orig = [] then List.map (fun b -> b.b_name) bhvs else orig
in
Kernel.warning ~once:true ~current:true
- "keeping only assigns from behaviors: %a"
- (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) orig
+ "keeping only assigns from behaviors: %a"
+ (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) orig
end;
a
-
+
(** Returns the assigns from complete behaviors and unguarded behaviors. *)
let merge_assigns_from_spec ?warn (spec :funspec) =
merge_assigns_from_complete_bhvs
@@ -256,21 +260,21 @@ let merge_assigns_from_spec ?warn (spec :funspec) =
(** Returns the assigns of an unguarded behavior. *)
let merge_assigns ?warn (bhvs : funbehavior list) =
let unguarded_bhvs = List.filter (fun b -> b.b_assumes = []) bhvs in
- let acc = merge_assigns_internal
- (fun b -> b.b_assigns) (fun b -> [b.b_name])
- None unguarded_bhvs
+ let acc = merge_assigns_internal
+ (fun b -> b.b_assigns) (fun b -> [b.b_name])
+ None unguarded_bhvs
in
match acc with
| None -> WritesAny (* No unguarded behavior -> assigns everything *)
| Some((a,(w,orig)),_) -> (* The smallest one *)
- let warn = match warn with
+ let warn = match warn with
| None -> w
- | Some warn -> warn
- in
+ | Some warn -> warn
+ in
if warn then
Kernel.warning ~once:true ~current:true
- "keeping only assigns from behaviors: %a"
- (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) orig;
+ "keeping only assigns from behaviors: %a"
+ (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) orig;
a
let variable_term loc v =
@@ -291,7 +295,7 @@ let constant_term loc i =
let rec is_null_term t = match t.term_node with
| TConst c when is_integral_logic_const c ->
- Integer.equal (value_of_integral_logic_const c) Integer.zero
+ Integer.equal (value_of_integral_logic_const c) Integer.zero
| TCastE(_,t) -> is_null_term t
| _ -> false
@@ -321,9 +325,9 @@ module Function = struct
let formal_args called_vinfo = match called_vinfo.vtype with
| TFun (_,Some argl,_,_) ->
- argl
+ argl
| TFun _ ->
- []
+ []
| _ -> assert false
let is_formal v fundec =
@@ -394,18 +398,18 @@ let array_type ?length ?(attr=[]) ty = TArray(ty,length,empty_size_cache (),attr
let direct_array_size ty =
match unrollType ty with
- | TArray(_ty,Some size,_,_) -> value_of_integral_expr size
- | TArray(_ty,None,_,_) -> Integer.zero
- | _ -> assert false
+ | TArray(_ty,Some size,_,_) -> value_of_integral_expr size
+ | TArray(_ty,None,_,_) -> Integer.zero
+ | _ -> assert false
let rec array_size ty =
match unrollType ty with
- | TArray(elemty,Some _,_,_) ->
- if isArrayType elemty then
- Integer.mul (direct_array_size ty) (array_size elemty)
- else direct_array_size ty
- | TArray(_,None,_,_) -> Integer.zero
- | _ -> assert false
+ | TArray(elemty,Some _,_,_) ->
+ if isArrayType elemty then
+ Integer.mul (direct_array_size ty) (array_size elemty)
+ else direct_array_size ty
+ | TArray(_,None,_,_) -> Integer.zero
+ | _ -> assert false
let direct_element_type ty = match unrollType ty with
| TArray(eltyp,_,_,_) -> eltyp
@@ -417,18 +421,18 @@ let element_type ty =
| _ -> ty
in
match unrollType ty with
- | TArray(eltyp,_,_,_) -> elem_type eltyp
- | _ -> assert false
+ | TArray(eltyp,_,_,_) -> elem_type eltyp
+ | _ -> assert false
let direct_pointed_type ty =
match unrollType ty with
- | TPtr(elemty,_) -> elemty
- | _ -> assert false
+ | TPtr(elemty,_) -> elemty
+ | _ -> assert false
let pointed_type ty =
match unrollType (direct_pointed_type ty) with
- | TArray _ as arrty -> element_type arrty
- | ty -> ty
+ | TArray _ as arrty -> element_type arrty
+ | ty -> ty
(* ************************************************************************** *)
(** {2 Predefined} *)
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 6d4ecc5dec010c913bd9890d7527ee471f25241c..22cef1f703033543f59da7d347470cd9e330fa71 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -62,56 +62,57 @@ val possible_value_of_integral_term: term -> Integer.t option
@since Oxygen-20120901 *)
val term_lvals_of_term: term -> term_lval list
- (** @return the list of all the term lvals of a given term.
- Purely syntactic function. *)
+(** @return the list of all the term lvals of a given term.
+ Purely syntactic function. *)
val precondition : funspec -> predicate
- (** Builds the precondition from [b_assumes] and [b_requires] clauses.
- @since Carbon-20101201 *)
+(** Builds the precondition from [b_assumes] and [b_requires] clauses.
+ @since Carbon-20101201 *)
val behavior_assumes : funbehavior -> predicate
- (** Builds the conjunction of the [b_assumes].
- @since Nitrogen-20111001 *)
-
+(** Builds the conjunction of the [b_assumes].
+ @since Nitrogen-20111001 *)
+
val behavior_precondition : funbehavior -> predicate
- (** Builds the precondition from [b_assumes] and [b_requires] clauses.
- @since Carbon-20101201 *)
+(** Builds the precondition from [b_assumes] and [b_requires] clauses.
+ @since Carbon-20101201 *)
val behavior_postcondition : funbehavior -> termination_kind -> predicate
- (** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
- @modify Boron-20100401 added termination kind as filtering argument. *)
+(** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
+ @modify Boron-20100401 added termination kind as filtering argument. *)
val disjoint_behaviors : funspec -> string list -> predicate
- (** Builds the [disjoint_behaviors] property for the behavior names.
- @since Nitrogen-20111001 *)
+(** Builds the [disjoint_behaviors] property for the behavior names.
+ @since Nitrogen-20111001 *)
val complete_behaviors : funspec -> string list -> predicate
- (** Builds the [disjoint_behaviors] property for the behavior names.
- @since Nitrogen-20111001 *)
+(** Builds the [disjoint_behaviors] property for the behavior names.
+ @since Nitrogen-20111001 *)
-val merge_assigns_from_complete_bhvs:
+val merge_assigns_from_complete_bhvs:
?warn:bool -> ?unguarded:bool -> funbehavior list -> string list list -> assigns
- (** @return the assigns of an unguarded behavior (when [unguarded]=true)
- or a set of complete behaviors.
- - the funbehaviors can come from either a statement contract or a function
- contract.
- - the list of sets of behavior names can come from the contract of the
+(** @return the assigns of an unguarded behavior (when [unguarded]=true)
+ or a set of complete behaviors.
+ - the funbehaviors can come from either a statement contract or a function
+ contract.
+ - the list of sets of behavior names can come from the contract of the
related function.
- Optional [warn] argument can be used to force emitting or cancelation of
- warnings.
- @since Oxygen-20120901 *)
+
+ Optional [warn] argument can be used to force emitting or cancelation of
+ warnings.
+ @since Oxygen-20120901 *)
val merge_assigns_from_spec: ?warn:bool -> funspec -> assigns
(** It is a shortcut for [merge_assigns_from_complete_bhvs
spec.spec_complete_behaviors spec.spec_behavior]. Optional [warn] argument
- can be used to force emitting or cancelation of warnings
+ can be used to force emitting or cancelation of warnings
@return the assigns of an unguarded behavior or a set of complete behaviors.
- @since Oxygen-20120901 *)
+ @since Oxygen-20120901 *)
val merge_assigns: ?warn:bool -> funbehavior list -> assigns
-(** Returns the assigns of an unguarded behavior.
+(** Returns the assigns of an unguarded behavior.
@modify Oxygen-20120901 Optional [warn] argument added which can be used to
- force emitting or cancelation of warnings. *)
+ force emitting or cancelation of warnings. *)
val variable_term: location -> logic_var -> term
val constant_term: location -> Integer.t -> term
@@ -153,21 +154,21 @@ val pointed_type: typ -> typ
(* ************************************************************************** *)
val is_function_type : varinfo -> bool
- (** Return [true] iff the type of the given varinfo is a function type. *)
+(** Return [true] iff the type of the given varinfo is a function type. *)
(** Operations on cil function. *)
module Function: sig
val formal_args: varinfo -> (string * typ * attributes) list
- (** Returns the list of the named formal arguments of a function.
- Never call on a variable of non functional type.*)
+ (** Returns the list of the named formal arguments of a function.
+ Never call on a variable of non functional type.*)
val is_formal: varinfo -> fundec -> bool
val is_local: varinfo -> fundec -> bool
val is_formal_or_local: varinfo -> fundec -> bool
val is_formal_of_prototype:
varinfo (* to check *) -> varinfo (* of the prototype *) -> bool
- (** [is_formal_of_prototype v f] returns [true] iff [f] is a prototype and
- [v] is one of its formal parameters. *)
+ (** [is_formal_of_prototype v f] returns [true] iff [f] is a prototype and
+ [v] is one of its formal parameters. *)
val is_definition: cil_function -> bool
val get_vi: cil_function -> varinfo
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 9192bb4f790dddd6d5b6a5bf14b379616ee9b377..0498ef145a6f1abd70ada90149e8b6a92cfd1e54 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -31,23 +31,23 @@ type cpp_opt_kind = Gnu | Not_gnu | Unknown
names given on the command line, without normalization. *)
type file =
| NeedCPP of Filepath.Normalized.t * string * cpp_opt_kind
- (** The first string is the filename of the [.c] to preprocess.
- The second one is the preprocessor command ([filename.c -o
- tempfilname.i] will be appended at the end).*)
+ (** The first string is the filename of the [.c] to preprocess.
+ The second one is the preprocessor command ([filename.c -o
+ tempfilname.i] will be appended at the end).*)
| NoCPP of Filepath.Normalized.t
- (** Already pre-processed file [.i] *)
+ (** Already pre-processed file [.i] *)
| External of Filepath.Normalized.t * string
- (** file that can be translated into a Cil AST through an external
- function, together with the recognized suffix. *)
+ (** file that can be translated into a Cil AST through an external
+ function, together with the recognized suffix. *)
include Datatype.S with type t = file
val new_file_type:
string -> (string -> Cil_types.file * Cabs.file) -> unit
- (** [new_file_type suffix func funcname] registers a new type of files (with
- corresponding suffix) as recognized by Frama-C through [func].
- @plugin development guide
- *)
+(** [new_file_type suffix func funcname] registers a new type of files (with
+ corresponding suffix) as recognized by Frama-C through [func].
+ @plugin development guide
+*)
val new_machdep: string -> Cil_types.mach -> unit
(** [new_machdep name module] registers a new machdep name as recognized by
@@ -61,152 +61,152 @@ val new_machdep: string -> Cil_types.mach -> unit
@plugin development guide *)
val machdep_macro: string -> string
- (** [machdep_macro machine] returns the name of a macro __FC_MACHDEP_XXX so
- that the preprocessor can select std lib definition consistent with
- the selected machdep. This function will emit a warning if [machine] is
- not known by default by the kernel and return __FC_MACHDEP_MACHINE in that
- case.
- @since Magnesium-20151001 (exported in the API)
- *)
+(** [machdep_macro machine] returns the name of a macro __FC_MACHDEP_XXX so
+ that the preprocessor can select std lib definition consistent with
+ the selected machdep. This function will emit a warning if [machine] is
+ not known by default by the kernel and return __FC_MACHDEP_MACHINE in that
+ case.
+ @since Magnesium-20151001 (exported in the API)
+*)
val list_available_machdeps: unit -> string list
(** [list_available_machdeps ()] gives the list of the names of available
machdeps, starting with the ones added with new_machdep and ending with
the list of default machdeps.
@since 22.0-Titanium *)
-
+
type code_transformation_category
(** type of registered code transformations
- @since Neon-20140301
+ @since Neon-20140301
*)
val register_code_transformation_category:
string -> code_transformation_category
(** Adds a new category of code transformation *)
-val add_code_transformation_before_cleanup:
+val add_code_transformation_before_cleanup:
?deps:(module Parameter_sig.S) list ->
?before:code_transformation_category list ->
?after:code_transformation_category list ->
code_transformation_category -> (Cil_types.file -> unit) -> unit
- (** [add_code_transformation_before_cleanup name hook]
- adds an hook in the corresponding category
- that will be called during the normalization of a linked
- file, before clean up and removal of temps and unused declarations.
- If this transformation involves changing statements of a function [f],
- [f] must be flagged with {!File.must_recompute_cfg}.
- The optional [before] (resp [after]) categories indicates that current
- transformation must be executed before (resp after)
- the corresponding ones, if they exist. In case of dependencies cycle,
- an arbitrary order will be chosen for the transformations involved in
- the cycle.
- The optional [deps] argument gives the list of options whose change
- (e.g. after a [-then]) will trigger the transformation over the already
- computed AST. If several transformations are triggered by the same
- option, their relative order is preserved.
-
- At this level, globals and ACSL annotations have not been registered.
-
- @since Neon-20140301
- @plugin development guide *)
+(** [add_code_transformation_before_cleanup name hook]
+ adds an hook in the corresponding category
+ that will be called during the normalization of a linked
+ file, before clean up and removal of temps and unused declarations.
+ If this transformation involves changing statements of a function [f],
+ [f] must be flagged with {!File.must_recompute_cfg}.
+ The optional [before] (resp [after]) categories indicates that current
+ transformation must be executed before (resp after)
+ the corresponding ones, if they exist. In case of dependencies cycle,
+ an arbitrary order will be chosen for the transformations involved in
+ the cycle.
+ The optional [deps] argument gives the list of options whose change
+ (e.g. after a [-then]) will trigger the transformation over the already
+ computed AST. If several transformations are triggered by the same
+ option, their relative order is preserved.
+
+ At this level, globals and ACSL annotations have not been registered.
+
+ @since Neon-20140301
+ @plugin development guide *)
val add_code_transformation_after_cleanup:
?deps:(module Parameter_sig.S) list ->
?before:code_transformation_category list ->
?after:code_transformation_category list ->
code_transformation_category -> (Cil_types.file -> unit) -> unit
- (** Same as above, but the hook is applied after clean up.
- At this level, globals and ACSL annotations have been registered. If
- the hook adds some new globals or annotations, it must take care of
- adding them in the appropriate tables.
- Note that it is the responsibility of the hook to use
- {!Ast.mark_as_changed} or {!Ast.mark_as_grown} whenever it is the case.
- @since Neon-20140301
- @plugin development guide *)
+(** Same as above, but the hook is applied after clean up.
+ At this level, globals and ACSL annotations have been registered. If
+ the hook adds some new globals or annotations, it must take care of
+ adding them in the appropriate tables.
+ Note that it is the responsibility of the hook to use
+ {!Ast.mark_as_changed} or {!Ast.mark_as_grown} whenever it is the case.
+ @since Neon-20140301
+ @plugin development guide *)
val constfold: code_transformation_category
(** category for syntactic constfolding (done after cleanup)
@since Silicon-20161101 *)
val must_recompute_cfg: Cil_types.fundec -> unit
- (** [must_recompute_cfg f] must be called by code transformation hooks
- when they modify statements in function [f]. This will trigger a
- recomputation of the cfg of [f] after the transformation.
- @since Neon-20140301
- @plugin development guide *)
+(** [must_recompute_cfg f] must be called by code transformation hooks
+ when they modify statements in function [f]. This will trigger a
+ recomputation of the cfg of [f] after the transformation.
+ @since Neon-20140301
+ @plugin development guide *)
val get_suffixes: unit -> string list
- (** @return the list of accepted suffixes of input source files
- @since Boron-20100401 *)
+(** @return the list of accepted suffixes of input source files
+ @since Boron-20100401 *)
val get_name: t -> string
- (** File name (not normalized). *)
+(** File name (not normalized). *)
val get_preprocessor_command: unit -> string * cpp_opt_kind
- (** Return the preprocessor command to use. *)
+(** Return the preprocessor command to use. *)
val pre_register: t -> unit
- (** Register some file as source file before command-line files *)
+(** Register some file as source file before command-line files *)
val get_all: unit -> t list
- (** Return the list of toplevel files. *)
+(** Return the list of toplevel files. *)
val from_filename: ?cpp:string -> Datatype.Filepath.t -> t
- (** Build a file from its name. The optional argument is the preprocessor
- command. Default is [!get_preprocessor_command ()]. *)
+(** Build a file from its name. The optional argument is the preprocessor
+ command. Default is [!get_preprocessor_command ()]. *)
(* ************************************************************************* *)
(** {2 Initializers} *)
(* ************************************************************************* *)
val prepare_from_c_files: unit -> unit
- (** Initialize the AST of the current project according to the current
- filename list.
- @raise File_types.Bad_Initialization if called more than once. *)
+(** Initialize the AST of the current project according to the current
+ filename list.
+ @raise File_types.Bad_Initialization if called more than once. *)
val init_from_c_files: t list -> unit
- (** Initialize the cil file representation of the current project.
- Should be called at most once per project.
- @raise File_types.Bad_Initialization if called more than once.
- @plugin development guide *)
+(** Initialize the cil file representation of the current project.
+ Should be called at most once per project.
+ @raise File_types.Bad_Initialization if called more than once.
+ @plugin development guide *)
val init_project_from_cil_file: Project.t -> Cil_types.file -> unit
- (** Initialize the cil file representation with the given file for the
- given project from the current one.
- Should be called at most once per project.
- @raise File_types.Bad_Initialization if called more than once.
- @plugin development guide *)
+(** Initialize the cil file representation with the given file for the
+ given project from the current one.
+ Should be called at most once per project.
+ @raise File_types.Bad_Initialization if called more than once.
+ @plugin development guide *)
val init_project_from_visitor:
?reorder:bool -> Project.t -> Visitor.frama_c_visitor -> unit
- (** [init_project_from_visitor prj vis] initialize the cil file
- representation of [prj]. [prj] must be essentially empty: it can have
- some options set, but not an existing cil file; [proj] is filled using
- [vis], which must be a copy visitor that puts its results in [prj].
- if [reorder] is [true] (default is [false]) the new AST in [prj]
- will be reordered.
- @since Oxygen-20120901
- @modify Fluorine-20130401 added reorder optional argument
- @plugin development guide
- *)
+(** [init_project_from_visitor prj vis] initialize the cil file
+ representation of [prj]. [prj] must be essentially empty: it can have
+ some options set, but not an existing cil file; [proj] is filled using
+ [vis], which must be a copy visitor that puts its results in [prj].
+ if [reorder] is [true] (default is [false]) the new AST in [prj]
+ will be reordered.
+ @since Oxygen-20120901
+ @modify Fluorine-20130401 added reorder optional argument
+ @plugin development guide
+*)
val create_project_from_visitor:
?reorder:bool -> ?last:bool ->
string ->
(Project.t -> Visitor.frama_c_visitor) ->
Project.t
- (** Return a new project with a new cil file representation by visiting the
- file of the current project. If [reorder] is [true], the globals in the
- AST of the new project are reordered (default is [false]). If [last] is
- [true] (by default), remember than the returned project is the last
- created one.
- The visitor is responsible to avoid sharing between old file and new
- file (i.e. it should use {!Cil.copy_visit} at some point).
- @raise File_types.Bad_Initialization if called more than once.
- @since Beryllium-20090601-beta1
- @modify Fluorine-20130401 added [reorder] optional argument
- @modify Sodium-20150201 added [last] optional argument
- @plugin development guide *)
+(** Return a new project with a new cil file representation by visiting the
+ file of the current project. If [reorder] is [true], the globals in the
+ AST of the new project are reordered (default is [false]). If [last] is
+ [true] (by default), remember than the returned project is the last
+ created one.
+ The visitor is responsible to avoid sharing between old file and new
+ file (i.e. it should use {!Cil.copy_visit} at some point).
+ @raise File_types.Bad_Initialization if called more than once.
+ @since Beryllium-20090601-beta1
+ @modify Fluorine-20130401 added [reorder] optional argument
+ @modify Sodium-20150201 added [last] optional argument
+ @plugin development guide *)
val create_rebuilt_project_from_visitor:
?reorder:bool -> ?last:bool -> ?preprocess:bool ->
@@ -221,7 +221,7 @@ val create_rebuilt_project_from_visitor:
NOT preprocessed by default.
@raise File_types.Bad_Initialization if called more than once.
- @since Nitrogen-20111001
+ @since Nitrogen-20111001
@modify Fluorine-20130401 added reorder optional argument
*)
@@ -236,10 +236,10 @@ val init_from_cmdline: unit -> unit
@plugin development guide *)
val reorder_ast: unit -> unit
- (** reorder globals so that all uses of an identifier are preceded by its
- declaration. This may introduce new declarations in the AST.
- @since Oxygen-20120901
- *)
+(** reorder globals so that all uses of an identifier are preceded by its
+ declaration. This may introduce new declarations in the AST.
+ @since Oxygen-20120901
+*)
val reorder_custom_ast: Cil_types.file -> unit
(** @since Neon-20140301 *)
@@ -250,14 +250,14 @@ val reorder_custom_ast: Cil_types.file -> unit
val pretty_machdep :
?fmt:Format.formatter -> ?machdep:Cil_types.mach -> unit -> unit
- (** Prints the associated [machdep], or the current one in current project
- by default. Default output formatter is [Log.print_on_output]. *)
+(** Prints the associated [machdep], or the current one in current project
+ by default. Default output formatter is [Log.print_on_output]. *)
val pretty_ast : ?prj:Project.t -> ?fmt:Format.formatter -> unit -> unit
- (** Print the project CIL file on the given Formatter.
- The default project is the current one.
- The default formatter is [Kernel.CodeOutput.get_fmt ()].
- @raise File_types.Bad_Initialization if the file is not initialized. *)
+(** Print the project CIL file on the given Formatter.
+ The default project is the current one.
+ The default formatter is [Kernel.CodeOutput.get_fmt ()].
+ @raise File_types.Bad_Initialization if the file is not initialized. *)
(*
Local Variables:
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index cc918e122f511db3fe8acf500aaaa9c701204b9f..6699fb861daad9d103af2806b0dc77bad33ee08b 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -48,790 +48,790 @@ end
annotations may not be visited properly. *)
class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c_visitor =
-object(self)
- inherit internal_genericCilVisitor fundec behavior queue
+ object(self)
+ inherit internal_genericCilVisitor fundec behavior queue
- method frama_c_plain_copy =
- new internal_generic_frama_c_visitor fundec queue current_kf behavior
+ method frama_c_plain_copy =
+ new internal_generic_frama_c_visitor fundec queue current_kf behavior
- method! plain_copy_visitor =
- assert (self#frama_c_plain_copy#get_filling_actions ==
+ method! plain_copy_visitor =
+ assert (self#frama_c_plain_copy#get_filling_actions ==
self#get_filling_actions);
- (self#frama_c_plain_copy :> Cil.cilVisitor)
-
- method set_current_kf kf = current_kf := Some kf
-
- method reset_current_kf () = current_kf := None
-
- method current_kf = !current_kf
-
- method! private vstmt stmt =
- let orig_stmt = Visitor_behavior.Get_orig.stmt self#behavior stmt in
- let annots =
- Annotations.fold_code_annot (fun e a acc -> (e, a) :: acc) orig_stmt []
- in
- let res = self#vstmt_aux stmt in
- (* Annotations will be visited and more importantly added in the
- same order as they were in the original AST. *)
- let annots =
- List.sort
- (fun (_,a) (_,b) -> Cil_datatype.Code_annotation.compare a b)
- annots
- in
- let make_children_annot vis =
- let add, remove =
- List.fold_left
- (fun (add, remove) (e, x) ->
- let y = visitCilCodeAnnotation (vis:>cilVisitor) x in
- (* Given x, we compute whether it must be removed from the
- destination project, and whether we should add its copy y,
- again in the destination project. *)
- let is_trivial = Logic_utils.is_trivial_annotation in
- (* we keep [y] only if it is non-trivial (non-\true), except
- if [x] is already trivial itself. *)
- let becomes_trivial = is_trivial y && not (is_trivial x) in
- let curr_add, remove_curr =
- if Visitor_behavior.is_copy vis#behavior then
- (* Copy visitor. We add [y], except if trivial. No sense in
- removing [x], since the stmt is a new one. *)
- (if not becomes_trivial then [e, y] else []),
- false
- else
- (* Inplace visitor. We remove [x] if it becomes trivial, or
- if it has changed (because we need to add it back with the
- new content). We re-add [y] if [x] has changed and has
- not became trivial. Do not always remove then re-add, as
- this would mess up property statuses. *)
- (if x != y && not becomes_trivial then [e, y] else []),
- (x != y || becomes_trivial)
- in
- (add @ curr_add, if remove_curr then (e, x) :: remove else remove)
- )
- ([],[])
+ (self#frama_c_plain_copy :> Cil.cilVisitor)
+
+ method set_current_kf kf = current_kf := Some kf
+
+ method reset_current_kf () = current_kf := None
+
+ method current_kf = !current_kf
+
+ method! private vstmt stmt =
+ let orig_stmt = Visitor_behavior.Get_orig.stmt self#behavior stmt in
+ let annots =
+ Annotations.fold_code_annot (fun e a acc -> (e, a) :: acc) orig_stmt []
+ in
+ let res = self#vstmt_aux stmt in
+ (* Annotations will be visited and more importantly added in the
+ same order as they were in the original AST. *)
+ let annots =
+ List.sort
+ (fun (_,a) (_,b) -> Cil_datatype.Code_annotation.compare a b)
annots
in
- (add, remove)
- in
- let change_stmt stmt (add, remove) =
- if (add <> [] || remove <> []) then begin
- let kf = Extlib.the self#current_kf in
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- Queue.add
- (fun () ->
- List.iter
- (fun (e, a) ->
- Annotations.remove_code_annot e ~kf:new_kf stmt a)
- remove;
- List.iter
- (fun (e, a) ->
- Annotations.add_code_annot
- ~keep_empty:false e ~kf:new_kf stmt a)
- add)
- self#get_filling_actions
- end
- in
- let post_action f stmt =
- let (add, _ as new_annots) = make_children_annot self in
- let stmt = f stmt in
- (match stmt.skind with
- | Block b when annots <> [] || add <> [] ->
- stmt.skind <- Block (Cil.block_of_transient b)
- | _ -> ());
- change_stmt stmt new_annots;
- stmt
- in
- let copy stmt =
- change_stmt stmt(make_children_annot self#frama_c_plain_copy);
- stmt
- in
- let plain_post = post_action (fun x -> x) in
- match res with
- | SkipChildren -> res
- | JustCopy -> JustCopyPost copy
- | JustCopyPost f -> JustCopyPost (f $ copy)
- | DoChildren -> DoChildrenPost plain_post
- | DoChildrenPost f -> DoChildrenPost (f $ plain_post)
- | ChangeTo _ | ChangeToPost _ -> res
- | ChangeDoChildrenPost (stmt,f) ->
- ChangeDoChildrenPost (stmt, post_action f)
-
- method vstmt_aux _ = DoChildren
- method vglob_aux _ = DoChildren
-
- method private vbehavior_annot ?e b =
- let kf = Extlib.the self#current_kf in
- let treat_elt emit elt acc =
- match e with
+ let make_children_annot vis =
+ let add, remove =
+ List.fold_left
+ (fun (add, remove) (e, x) ->
+ let y = visitCilCodeAnnotation (vis:>cilVisitor) x in
+ (* Given x, we compute whether it must be removed from the
+ destination project, and whether we should add its copy y,
+ again in the destination project. *)
+ let is_trivial = Logic_utils.is_trivial_annotation in
+ (* we keep [y] only if it is non-trivial (non-\true), except
+ if [x] is already trivial itself. *)
+ let becomes_trivial = is_trivial y && not (is_trivial x) in
+ let curr_add, remove_curr =
+ if Visitor_behavior.is_copy vis#behavior then
+ (* Copy visitor. We add [y], except if trivial. No sense in
+ removing [x], since the stmt is a new one. *)
+ (if not becomes_trivial then [e, y] else []),
+ false
+ else
+ (* Inplace visitor. We remove [x] if it becomes trivial, or
+ if it has changed (because we need to add it back with the
+ new content). We re-add [y] if [x] has changed and has
+ not became trivial. Do not always remove then re-add, as
+ this would mess up property statuses. *)
+ (if x != y && not becomes_trivial then [e, y] else []),
+ (x != y || becomes_trivial)
+ in
+ (add @ curr_add, if remove_curr then (e, x) :: remove else remove)
+ )
+ ([],[])
+ annots
+ in
+ (add, remove)
+ in
+ let change_stmt stmt (add, remove) =
+ if (add <> [] || remove <> []) then begin
+ let kf = Extlib.the self#current_kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ Queue.add
+ (fun () ->
+ List.iter
+ (fun (e, a) ->
+ Annotations.remove_code_annot e ~kf:new_kf stmt a)
+ remove;
+ List.iter
+ (fun (e, a) ->
+ Annotations.add_code_annot
+ ~keep_empty:false e ~kf:new_kf stmt a)
+ add)
+ self#get_filling_actions
+ end
+ in
+ let post_action f stmt =
+ let (add, _ as new_annots) = make_children_annot self in
+ let stmt = f stmt in
+ (match stmt.skind with
+ | Block b when annots <> [] || add <> [] ->
+ stmt.skind <- Block (Cil.block_of_transient b)
+ | _ -> ());
+ change_stmt stmt new_annots;
+ stmt
+ in
+ let copy stmt =
+ change_stmt stmt(make_children_annot self#frama_c_plain_copy);
+ stmt
+ in
+ let plain_post = post_action (fun x -> x) in
+ match res with
+ | SkipChildren -> res
+ | JustCopy -> JustCopyPost copy
+ | JustCopyPost f -> JustCopyPost (f $ copy)
+ | DoChildren -> DoChildrenPost plain_post
+ | DoChildrenPost f -> DoChildrenPost (f $ plain_post)
+ | ChangeTo _ | ChangeToPost _ -> res
+ | ChangeDoChildrenPost (stmt,f) ->
+ ChangeDoChildrenPost (stmt, post_action f)
+
+ method vstmt_aux _ = DoChildren
+ method vglob_aux _ = DoChildren
+
+ method private vbehavior_annot ?e b =
+ let kf = Extlib.the self#current_kf in
+ let treat_elt emit elt acc =
+ match e with
| None -> (emit, elt) :: acc
| Some e when Emitter.equal e emit -> (emit, elt) :: acc
| Some _ -> acc
- in
- let fold_elt fold = fold treat_elt kf b.b_name [] in
- let old_requires = fold_elt Annotations.fold_requires in
- let old_assumes = fold_elt Annotations.fold_assumes in
- let old_ensures = fold_elt Annotations.fold_ensures in
- let old_assigns = fold_elt Annotations.fold_assigns in
- let old_allocates = fold_elt Annotations.fold_allocates in
- let old_extended = fold_elt Annotations.fold_extended in
- let b' =
- if Visitor_behavior.is_copy self#behavior then
- { b with b_name = b.b_name }
- else b
- in
- let res = self#vbehavior b' in
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- let add_queue a = Queue.add a self#get_filling_actions in
- let visit_clauses vis f =
- (* Ensures that we have a table associated to new_kf in Annotations. *)
- add_queue
- (fun () ->
- ignore (Annotations.behaviors ~populate:false new_kf));
- let module Fold =
- struct
- type 'a t =
- { apply: 'b. (Emitter.t -> 'a -> 'b -> 'b) ->
- Kernel_function.t -> string -> 'b -> 'b }
- end
in
- let visit_elt visit e elt (f,acc) =
- let new_elt = visit (vis:>Cil.cilVisitor) elt in
- (* We'll add the elts afterwards, so as to keep lists in their
- original order as much as we can. see fold_elt below.
- *)
- f || new_elt != elt || new_kf != kf,
- (e,new_elt) :: acc
+ let fold_elt fold = fold treat_elt kf b.b_name [] in
+ let old_requires = fold_elt Annotations.fold_requires in
+ let old_assumes = fold_elt Annotations.fold_assumes in
+ let old_ensures = fold_elt Annotations.fold_ensures in
+ let old_assigns = fold_elt Annotations.fold_assigns in
+ let old_allocates = fold_elt Annotations.fold_allocates in
+ let old_extended = fold_elt Annotations.fold_extended in
+ let b' =
+ if Visitor_behavior.is_copy self#behavior then
+ { b with b_name = b.b_name }
+ else b
in
- let check_elt visit e' elt acc =
- match e with
+ let res = self#vbehavior b' in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ let add_queue a = Queue.add a self#get_filling_actions in
+ let visit_clauses vis f =
+ (* Ensures that we have a table associated to new_kf in Annotations. *)
+ add_queue
+ (fun () ->
+ ignore (Annotations.behaviors ~populate:false new_kf));
+ let module Fold =
+ struct
+ type 'a t =
+ { apply: 'b. (Emitter.t -> 'a -> 'b -> 'b) ->
+ Kernel_function.t -> string -> 'b -> 'b }
+ end
+ in
+ let visit_elt visit e elt (f,acc) =
+ let new_elt = visit (vis:>Cil.cilVisitor) elt in
+ (* We'll add the elts afterwards, so as to keep lists in their
+ original order as much as we can. see fold_elt below.
+ *)
+ f || new_elt != elt || new_kf != kf,
+ (e,new_elt) :: acc
+ in
+ let check_elt visit e' elt acc =
+ match e with
| None -> visit_elt visit e' elt acc
| Some e when Emitter.equal e e' -> visit_elt visit e' elt acc
| Some _ -> acc
- in
- let fold_elt fold visit remove add append dft =
- let (changed, res) =
- fold.Fold.apply (check_elt visit) kf b'.b_name (false,[])
in
- if changed then begin
- add_queue
- (fun () ->
- fold.Fold.apply
- (fun e' x () ->
- match e with
- | None -> remove e' new_kf x
- | Some e when Emitter.equal e e' -> remove e' new_kf x
- | _ -> ())
- new_kf b'.b_name ();
- List.iter (fun (e,x) -> add e new_kf b'.b_name x) res)
- end;
- List.fold_left (fun acc (_,x) -> append x acc) dft res
- in
- let req =
- fold_elt
- { Fold.apply = Annotations.fold_requires }
- Cil.visitCilIdPredicate
- Annotations.remove_requires
- (fun e kf behavior r -> Annotations.add_requires e kf ~behavior [r])
- (fun x l -> x :: l) []
- in
- b'.b_requires <- req;
- let assumes =
- fold_elt
- { Fold.apply = Annotations.fold_assumes }
- Cil.visitCilIdPredicate
- Annotations.remove_assumes
- (fun e kf behavior a -> Annotations.add_assumes e kf ~behavior [a])
- (fun x l -> x :: l) []
- in
- b'.b_assumes <- assumes;
- let visit_ensures vis (k,p as e) =
- let new_p = Cil.visitCilIdPredicate (vis:>Cil.cilVisitor) p in
- if p != new_p then (k,new_p) else e
- in
- let ensures =
- fold_elt
- { Fold.apply = Annotations.fold_ensures }
- visit_ensures
- Annotations.remove_ensures
- (fun e kf behavior p -> Annotations.add_ensures e kf ~behavior [p])
- (fun x l -> x :: l) []
- in
- b'.b_post_cond <- ensures;
- let add_assigns e kf behavior a =
- match a with
+ let fold_elt fold visit remove add append dft =
+ let (changed, res) =
+ fold.Fold.apply (check_elt visit) kf b'.b_name (false,[])
+ in
+ if changed then begin
+ add_queue
+ (fun () ->
+ fold.Fold.apply
+ (fun e' x () ->
+ match e with
+ | None -> remove e' new_kf x
+ | Some e when Emitter.equal e e' -> remove e' new_kf x
+ | _ -> ())
+ new_kf b'.b_name ();
+ List.iter (fun (e,x) -> add e new_kf b'.b_name x) res)
+ end;
+ List.fold_left (fun acc (_,x) -> append x acc) dft res
+ in
+ let req =
+ fold_elt
+ { Fold.apply = Annotations.fold_requires }
+ Cil.visitCilIdPredicate
+ Annotations.remove_requires
+ (fun e kf behavior r -> Annotations.add_requires e kf ~behavior [r])
+ (fun x l -> x :: l) []
+ in
+ b'.b_requires <- req;
+ let assumes =
+ fold_elt
+ { Fold.apply = Annotations.fold_assumes }
+ Cil.visitCilIdPredicate
+ Annotations.remove_assumes
+ (fun e kf behavior a -> Annotations.add_assumes e kf ~behavior [a])
+ (fun x l -> x :: l) []
+ in
+ b'.b_assumes <- assumes;
+ let visit_ensures vis (k,p as e) =
+ let new_p = Cil.visitCilIdPredicate (vis:>Cil.cilVisitor) p in
+ if p != new_p then (k,new_p) else e
+ in
+ let ensures =
+ fold_elt
+ { Fold.apply = Annotations.fold_ensures }
+ visit_ensures
+ Annotations.remove_ensures
+ (fun e kf behavior p -> Annotations.add_ensures e kf ~behavior [p])
+ (fun x l -> x :: l) []
+ in
+ b'.b_post_cond <- ensures;
+ let add_assigns e kf behavior a =
+ match a with
| WritesAny -> ()
| _ -> Annotations.add_assigns ~keep_empty:false e kf ~behavior a
- in
- let concat_assigns new_a a =
- match new_a, a with
+ in
+ let concat_assigns new_a a =
+ match new_a, a with
| WritesAny, a | a, WritesAny -> a
| Writes a1, Writes a2 -> Writes (a2 @ a1)
- in
- let a =
- fold_elt
- { Fold.apply = Annotations.fold_assigns }
- Cil.visitCilAssigns
- Annotations.remove_assigns
- add_assigns
- concat_assigns
- WritesAny
- in
- b'.b_assigns <- a;
- let concat_allocation new_a a =
- match new_a, a with
+ in
+ let a =
+ fold_elt
+ { Fold.apply = Annotations.fold_assigns }
+ Cil.visitCilAssigns
+ Annotations.remove_assigns
+ add_assigns
+ concat_assigns
+ WritesAny
+ in
+ b'.b_assigns <- a;
+ let concat_allocation new_a a =
+ match new_a, a with
| FreeAllocAny, a | a, FreeAllocAny -> a
| FreeAlloc(a1,a2), FreeAlloc(a3,a4) -> FreeAlloc (a3@a1,a4@a2)
+ in
+ let a =
+ fold_elt
+ { Fold.apply = Annotations.fold_allocates }
+ Cil.visitCilAllocation
+ Annotations.remove_allocates
+ (fun e kf behavior a ->
+ Annotations.add_allocates ~keep_empty:false e kf ~behavior a)
+ concat_allocation
+ FreeAllocAny
+ in
+ b'.b_allocation <- a;
+ let ext =
+ fold_elt
+ { Fold.apply = Annotations.fold_extended }
+ Cil.visitCilExtended
+ Annotations.remove_extended
+ (fun e kf behavior ex -> Annotations.add_extended e kf ~behavior ex)
+ (fun x y -> x::y)
+ []
+ in
+ b'.b_extended <- ext;
+ f b'
+ in
+ let remove_and_add get remove add fold old b =
+ let emitter = match e with None -> Emitter.end_user | Some e -> e in
+ let elts = get b in
+ List.iter
+ (fun (e,x) ->
+ if not (List.memq x elts) then
+ add_queue (fun () -> remove e new_kf x))
+ old;
+ let module M = struct exception Found of Emitter.t end in
+ let already_there x =
+ fold (fun e y () -> if x == y then raise (M.Found e)) new_kf b.b_name ()
+ in
+ List.iter
+ (fun x ->
+ add_queue
+ (fun () ->
+ try
+ already_there x;
+ add emitter new_kf b.b_name x
+ with M.Found e ->
+ (* We keep x at its right place inside b. *)
+ remove e new_kf x;
+ add e new_kf b.b_name x))
+ (List.rev elts);
in
- let a =
- fold_elt
- { Fold.apply = Annotations.fold_allocates }
- Cil.visitCilAllocation
+ let register_annots b' f =
+ add_queue
+ (fun () -> ignore (Annotations.behaviors ~populate:false new_kf));
+ remove_and_add
+ (fun b -> b.b_requires)
+ Annotations.remove_requires
+ (fun e kf behavior r -> Annotations.add_requires e kf ~behavior [r])
+ Annotations.fold_requires
+ old_requires b';
+ remove_and_add
+ (fun b -> b.b_assumes)
+ Annotations.remove_assumes
+ (fun e kf behavior r -> Annotations.add_assumes e kf ~behavior [r])
+ Annotations.fold_assumes
+ old_assumes b';
+ remove_and_add
+ (fun b -> b.b_post_cond)
+ Annotations.remove_ensures
+ (fun e kf behavior r -> Annotations.add_ensures e kf ~behavior [r])
+ Annotations.fold_ensures
+ old_ensures b';
+ remove_and_add
+ (fun b -> match b.b_assigns with WritesAny -> [] | a -> [a])
+ Annotations.remove_assigns
+ (fun e kf behavior a ->
+ match a with
+ | WritesAny -> ()
+ | Writes _ ->
+ Annotations.add_assigns ~keep_empty:false e kf ~behavior a)
+ Annotations.fold_assigns
+ old_assigns b';
+ remove_and_add
+ (fun b -> match b.b_allocation with FreeAllocAny -> [] | a -> [a])
Annotations.remove_allocates
(fun e kf behavior a ->
Annotations.add_allocates ~keep_empty:false e kf ~behavior a)
- concat_allocation
- FreeAllocAny
- in
- b'.b_allocation <- a;
- let ext =
- fold_elt
- { Fold.apply = Annotations.fold_extended }
- Cil.visitCilExtended
+ Annotations.fold_allocates
+ old_allocates b';
+ remove_and_add
+ (fun b -> b.b_extended)
Annotations.remove_extended
(fun e kf behavior ex -> Annotations.add_extended e kf ~behavior ex)
- (fun x y -> x::y)
- []
+ Annotations.fold_extended
+ old_extended b';
+ f b'
in
- b'.b_extended <- ext;
- f b'
- in
- let remove_and_add get remove add fold old b =
- let emitter = match e with None -> Emitter.end_user | Some e -> e in
- let elts = get b in
- List.iter
- (fun (e,x) ->
- if not (List.memq x elts) then
- add_queue (fun () -> remove e new_kf x))
- old;
- let module M = struct exception Found of Emitter.t end in
- let already_there x =
- fold (fun e y () -> if x == y then raise (M.Found e)) new_kf b.b_name ()
- in
- List.iter
- (fun x ->
- add_queue
- (fun () ->
- try
- already_there x;
- add emitter new_kf b.b_name x
- with M.Found e ->
- (* We keep x at its right place inside b. *)
- remove e new_kf x;
- add e new_kf b.b_name x))
- (List.rev elts);
- in
- let register_annots b' f =
- add_queue
- (fun () -> ignore (Annotations.behaviors ~populate:false new_kf));
- remove_and_add
- (fun b -> b.b_requires)
- Annotations.remove_requires
- (fun e kf behavior r -> Annotations.add_requires e kf ~behavior [r])
- Annotations.fold_requires
- old_requires b';
- remove_and_add
- (fun b -> b.b_assumes)
- Annotations.remove_assumes
- (fun e kf behavior r -> Annotations.add_assumes e kf ~behavior [r])
- Annotations.fold_assumes
- old_assumes b';
- remove_and_add
- (fun b -> b.b_post_cond)
- Annotations.remove_ensures
- (fun e kf behavior r -> Annotations.add_ensures e kf ~behavior [r])
- Annotations.fold_ensures
- old_ensures b';
- remove_and_add
- (fun b -> match b.b_assigns with WritesAny -> [] | a -> [a])
- Annotations.remove_assigns
- (fun e kf behavior a ->
- match a with
- | WritesAny -> ()
- | Writes _ ->
- Annotations.add_assigns ~keep_empty:false e kf ~behavior a)
- Annotations.fold_assigns
- old_assigns b';
- remove_and_add
- (fun b -> match b.b_allocation with FreeAllocAny -> [] | a -> [a])
- Annotations.remove_allocates
- (fun e kf behavior a ->
- Annotations.add_allocates ~keep_empty:false e kf ~behavior a)
- Annotations.fold_allocates
- old_allocates b';
- remove_and_add
- (fun b -> b.b_extended)
- Annotations.remove_extended
- (fun e kf behavior ex -> Annotations.add_extended e kf ~behavior ex)
- Annotations.fold_extended
- old_extended b';
- f b'
- in
- match res with
+ match res with
| SkipChildren -> b
| JustCopy -> visit_clauses self#plain_copy_visitor Extlib.id
| JustCopyPost f -> visit_clauses self#plain_copy_visitor f
| ChangeTo b -> register_annots b Extlib.id
| ChangeToPost (b,f) -> register_annots b f
| ChangeDoChildrenPost (b,f) ->
- register_annots (Cil.childrenBehavior (self:>Cil.cilVisitor) b) f
+ register_annots (Cil.childrenBehavior (self:>Cil.cilVisitor) b) f
| DoChildren -> visit_clauses self Extlib.id
| DoChildrenPost f -> visit_clauses self f
- method private vfunspec_annot () =
- let kf = Extlib.the self#current_kf in
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- let old_behaviors =
- Annotations.fold_behaviors (fun e b acc -> (e,b)::acc) kf []
- in
- let old_complete =
- Annotations.fold_complete (fun e c acc -> (e,c)::acc) kf []
- in
- let old_disjoint =
- Annotations.fold_disjoint (fun e d acc -> (e,d)::acc) kf []
- in
- let old_terminates =
- Annotations.fold_terminates (fun e t _ -> Some (e,t)) kf None
- in
- let old_decreases =
- Annotations.fold_decreases (fun e d _ -> Some (e,d)) kf None
- in
- let spec =
- { spec_behavior = snd (List.split old_behaviors);
- spec_complete_behaviors = snd (List.split old_complete);
- spec_disjoint_behaviors = snd (List.split old_disjoint);
- spec_terminates =
- (Extlib.opt_map snd) old_terminates;
- spec_variant =
- (Extlib.opt_map snd) old_decreases
- }
- in
- let res = self#vspec spec in
- let do_children () =
- let new_behaviors =
- List.rev_map
- (fun (e,b) ->
- let b' = self#vbehavior_annot ~e b in
- if b != b' || kf != new_kf then begin
- Queue.add
- (fun () ->
- Annotations.add_behaviors
- ~register_children:false e new_kf [b'])
- self#get_filling_actions;
- end;
- b')
- old_behaviors
+ method private vfunspec_annot () =
+ let kf = Extlib.the self#current_kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ let old_behaviors =
+ Annotations.fold_behaviors (fun e b acc -> (e,b)::acc) kf []
in
- let new_terminates =
- Extlib.opt_map
- (fun (e,t) ->
- let t' = Cil.visitCilIdPredicate (self:>Cil.cilVisitor) t in
- if t != t' || kf != new_kf then
- Queue.add (fun () ->
- Annotations.remove_terminates e new_kf;
- Annotations.add_terminates e new_kf t')
- self#get_filling_actions
- ;
- t')
- old_terminates
+ let old_complete =
+ Annotations.fold_complete (fun e c acc -> (e,c)::acc) kf []
in
- let new_decreases =
- Extlib.opt_map
- (fun (e,(d,s as acc)) ->
- let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
- if d != d' || kf != new_kf then begin
- let res = (d',s) in
- Queue.add
- (fun () ->
- Annotations.remove_decreases e new_kf;
- Annotations.add_decreases e new_kf res;
- )
- self#get_filling_actions;
- res
- end else acc
- )
- old_decreases
+ let old_disjoint =
+ Annotations.fold_disjoint (fun e d acc -> (e,d)::acc) kf []
in
- if kf != new_kf then begin
- List.iter
- (fun (e,c) ->
- Queue.add (fun () -> Annotations.add_complete e new_kf c)
- self#get_filling_actions)
- (List.rev old_complete);
- List.iter
- (fun (e,d) ->
- Queue.add (fun () -> Annotations.add_disjoint e new_kf d)
- self#get_filling_actions)
- (List.rev old_disjoint)
- end;
- { spec with
- spec_behavior = new_behaviors;
- spec_terminates = new_terminates;
- spec_variant = new_decreases }
- in
- let change_do_children spec =
- let new_behaviors =
- Cil.mapNoCopy self#vbehavior_annot spec.spec_behavior
+ let old_terminates =
+ Annotations.fold_terminates (fun e t _ -> Some (e,t)) kf None
in
- let new_terminates =
- Cil.optMapNoCopy (Cil.visitCilIdPredicate (self:>Cil.cilVisitor))
- spec.spec_terminates
+ let old_decreases =
+ Annotations.fold_decreases (fun e d _ -> Some (e,d)) kf None
in
- let new_decreases =
- Cil.optMapNoCopy
- (fun (d,s as acc) ->
- let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
- if d != d' then (d',s) else acc)
- spec.spec_variant
+ let spec =
+ { spec_behavior = snd (List.split old_behaviors);
+ spec_complete_behaviors = snd (List.split old_complete);
+ spec_disjoint_behaviors = snd (List.split old_disjoint);
+ spec_terminates =
+ (Extlib.opt_map snd) old_terminates;
+ spec_variant =
+ (Extlib.opt_map snd) old_decreases
+ }
in
- { spec with
- spec_behavior = new_behaviors;
- spec_terminates = new_terminates;
- spec_variant = new_decreases }
- in
- let register_new_components new_spec =
- let add_spec_components () =
- let populate = false in
- let new_behaviors = Annotations.behaviors ~populate new_kf in
+ let res = self#vspec spec in
+ let do_children () =
+ let new_behaviors =
+ List.rev_map
+ (fun (e,b) ->
+ let b' = self#vbehavior_annot ~e b in
+ if b != b' || kf != new_kf then begin
+ Queue.add
+ (fun () ->
+ Annotations.add_behaviors
+ ~register_children:false e new_kf [b'])
+ self#get_filling_actions;
+ end;
+ b')
+ old_behaviors
+ in
+ let new_terminates =
+ Extlib.opt_map
+ (fun (e,t) ->
+ let t' = Cil.visitCilIdPredicate (self:>Cil.cilVisitor) t in
+ if t != t' || kf != new_kf then
+ Queue.add (fun () ->
+ Annotations.remove_terminates e new_kf;
+ Annotations.add_terminates e new_kf t')
+ self#get_filling_actions
+ ;
+ t')
+ old_terminates
+ in
+ let new_decreases =
+ Extlib.opt_map
+ (fun (e,(d,s as acc)) ->
+ let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
+ if d != d' || kf != new_kf then begin
+ let res = (d',s) in
+ Queue.add
+ (fun () ->
+ Annotations.remove_decreases e new_kf;
+ Annotations.add_decreases e new_kf res;
+ )
+ self#get_filling_actions;
+ res
+ end else acc
+ )
+ old_decreases
+ in
+ if kf != new_kf then begin
+ List.iter
+ (fun (e,c) ->
+ Queue.add (fun () -> Annotations.add_complete e new_kf c)
+ self#get_filling_actions)
+ (List.rev old_complete);
+ List.iter
+ (fun (e,d) ->
+ Queue.add (fun () -> Annotations.add_disjoint e new_kf d)
+ self#get_filling_actions)
+ (List.rev old_disjoint)
+ end;
+ { spec with
+ spec_behavior = new_behaviors;
+ spec_terminates = new_terminates;
+ spec_variant = new_decreases }
+ in
+ let change_do_children spec =
+ let new_behaviors =
+ Cil.mapNoCopy self#vbehavior_annot spec.spec_behavior
+ in
+ let new_terminates =
+ Cil.optMapNoCopy (Cil.visitCilIdPredicate (self:>Cil.cilVisitor))
+ spec.spec_terminates
+ in
+ let new_decreases =
+ Cil.optMapNoCopy
+ (fun (d,s as acc) ->
+ let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
+ if d != d' then (d',s) else acc)
+ spec.spec_variant
+ in
+ { spec with
+ spec_behavior = new_behaviors;
+ spec_terminates = new_terminates;
+ spec_variant = new_decreases }
+ in
+ let register_new_components new_spec =
+ let add_spec_components () =
+ let populate = false in
+ let new_behaviors = Annotations.behaviors ~populate new_kf in
+ List.iter
+ (fun b ->
+ if
+ (List.for_all
+ (fun x -> x.b_name <> b.b_name || Cil.is_empty_behavior x)
+ new_behaviors)
+ then begin
+ Annotations.add_behaviors ~register_children:false
+ Emitter.end_user new_kf [b]
+ end)
+ new_spec.spec_behavior;
+ let new_complete = Annotations.complete ~populate new_kf in
+ List.iter
+ (fun c ->
+ if not (List.memq c new_complete) then begin
+ Annotations.add_complete Emitter.end_user new_kf c
+ end)
+ new_spec.spec_complete_behaviors;
+ let new_disjoint = Annotations.disjoint ~populate new_kf in
+ List.iter
+ (fun d ->
+ if not (List.memq d new_disjoint) then
+ Annotations.add_disjoint Emitter.end_user new_kf d)
+ new_spec.spec_disjoint_behaviors;
+ let new_terminates = Annotations.terminates ~populate new_kf in
+ (match new_terminates, new_spec.spec_terminates with
+ | None, None -> ()
+ | Some _, None -> ()
+ | None, Some p ->
+ Annotations.add_terminates Emitter.end_user new_kf p
+ | Some p1, Some p2 when p1 == p2 -> ()
+ | Some p1, Some p2 ->
+ Kernel.fatal
+ "Visit of spec of function %a gives \
+ inconsistent terminates clauses@\n\
+ Registered @[%a@]@\nReturned @[%a@]"
+ Kernel_function.pretty new_kf
+ Printer.pp_identified_predicate p1
+ Printer.pp_identified_predicate p2);
+ let new_decreases = Annotations.decreases ~populate new_kf in
+ (match new_decreases, new_spec.spec_variant with
+ | None, None -> ()
+ | Some _, None -> ()
+ | None, Some p ->
+ Annotations.add_decreases Emitter.end_user new_kf p
+ | Some p1, Some p2 when p1 == p2 -> ()
+ | Some p1, Some p2 ->
+ Kernel.fatal
+ "Visit of spec of function %a gives \
+ inconsistent variant clauses@\n\
+ Registered %d@\n%a@\nReturned %d@\n%a"
+ Kernel_function.pretty new_kf
+ (Obj.magic p1)
+ Printer.pp_decreases p1
+ (Obj.magic p2)
+ Printer.pp_decreases p2)
+ in
List.iter
- (fun b ->
- if
- (List.for_all
- (fun x -> x.b_name <> b.b_name || Cil.is_empty_behavior x)
- new_behaviors)
- then begin
- Annotations.add_behaviors ~register_children:false
- Emitter.end_user new_kf [b]
- end)
- new_spec.spec_behavior;
- let new_complete = Annotations.complete ~populate new_kf in
+ (fun (e,c) ->
+ if not (List.memq c new_spec.spec_complete_behaviors) then
+ Queue.add
+ (fun () -> Annotations.remove_complete e new_kf c)
+ self#get_filling_actions)
+ old_complete;
List.iter
- (fun c ->
- if not (List.memq c new_complete) then begin
- Annotations.add_complete Emitter.end_user new_kf c
- end)
- new_spec.spec_complete_behaviors;
- let new_disjoint = Annotations.disjoint ~populate new_kf in
+ (fun (e,d) ->
+ if not (List.memq d new_spec.spec_disjoint_behaviors) then
+ Queue.add
+ (fun () -> Annotations.remove_disjoint e new_kf d)
+ self#get_filling_actions)
+ old_disjoint;
List.iter
- (fun d ->
- if not (List.memq d new_disjoint) then
- Annotations.add_disjoint Emitter.end_user new_kf d)
- new_spec.spec_disjoint_behaviors;
- let new_terminates = Annotations.terminates ~populate new_kf in
- (match new_terminates, new_spec.spec_terminates with
- | None, None -> ()
- | Some _, None -> ()
- | None, Some p ->
- Annotations.add_terminates Emitter.end_user new_kf p
- | Some p1, Some p2 when p1 == p2 -> ()
- | Some p1, Some p2 ->
- Kernel.fatal
- "Visit of spec of function %a gives \
- inconsistent terminates clauses@\n\
- Registered @[%a@]@\nReturned @[%a@]"
- Kernel_function.pretty new_kf
- Printer.pp_identified_predicate p1
- Printer.pp_identified_predicate p2);
- let new_decreases = Annotations.decreases ~populate new_kf in
- (match new_decreases, new_spec.spec_variant with
- | None, None -> ()
- | Some _, None -> ()
- | None, Some p ->
- Annotations.add_decreases Emitter.end_user new_kf p
- | Some p1, Some p2 when p1 == p2 -> ()
- | Some p1, Some p2 ->
- Kernel.fatal
- "Visit of spec of function %a gives \
- inconsistent variant clauses@\n\
- Registered %d@\n%a@\nReturned %d@\n%a"
- Kernel_function.pretty new_kf
- (Obj.magic p1)
- Printer.pp_decreases p1
- (Obj.magic p2)
- Printer.pp_decreases p2)
+ (fun (e,b) ->
+ if not (List.memq b new_spec.spec_behavior) then begin
+ Queue.add
+ (fun () ->
+ if
+ List.exists (fun x -> x.b_name = b.b_name)
+ new_spec.spec_behavior
+ then Annotations.remove_behavior_components e new_kf b
+ else Annotations.remove_behavior e new_kf b)
+ self#get_filling_actions
+ end
+ )
+ old_behaviors;
+ Extlib.may
+ (fun (e,t) ->
+ if not (Extlib.may_map
+ ~dft:false (fun t' -> t == t') new_spec.spec_terminates)
+ then
+ Queue.add
+ (fun () -> Annotations.remove_terminates e new_kf)
+ self#get_filling_actions)
+ old_terminates;
+ Extlib.may
+ (fun (e,d) ->
+ if not (Extlib.may_map
+ ~dft:false (fun d' -> d == d') new_spec.spec_variant)
+ then
+ Queue.add
+ (fun () -> Annotations.remove_decreases e new_kf)
+ self#get_filling_actions)
+ old_decreases;
+ Queue.add add_spec_components self#get_filling_actions;
in
- List.iter
- (fun (e,c) ->
- if not (List.memq c new_spec.spec_complete_behaviors) then
- Queue.add
- (fun () -> Annotations.remove_complete e new_kf c)
- self#get_filling_actions)
- old_complete;
- List.iter
- (fun (e,d) ->
- if not (List.memq d new_spec.spec_disjoint_behaviors) then
- Queue.add
- (fun () -> Annotations.remove_disjoint e new_kf d)
- self#get_filling_actions)
- old_disjoint;
- List.iter
- (fun (e,b) ->
- if not (List.memq b new_spec.spec_behavior) then begin
- Queue.add
- (fun () ->
- if
- List.exists (fun x -> x.b_name = b.b_name)
- new_spec.spec_behavior
- then Annotations.remove_behavior_components e new_kf b
- else Annotations.remove_behavior e new_kf b)
- self#get_filling_actions
- end
- )
- old_behaviors;
- Extlib.may
- (fun (e,t) ->
- if not (Extlib.may_map
- ~dft:false (fun t' -> t == t') new_spec.spec_terminates)
- then
- Queue.add
- (fun () -> Annotations.remove_terminates e new_kf)
- self#get_filling_actions)
- old_terminates;
- Extlib.may
- (fun (e,d) ->
- if not (Extlib.may_map
- ~dft:false (fun d' -> d == d') new_spec.spec_variant)
- then
- Queue.add
- (fun () -> Annotations.remove_decreases e new_kf)
- self#get_filling_actions)
- old_decreases;
- Queue.add add_spec_components self#get_filling_actions;
- in
- match res with
+ match res with
| SkipChildren -> register_new_components spec
| ChangeTo spec -> register_new_components spec
- | ChangeToPost (spec,f) ->
- register_new_components spec; ignore (f spec)
+ | ChangeToPost (spec,f) ->
+ register_new_components spec; ignore (f spec)
| JustCopy ->
- register_new_components
- (Cil.visitCilFunspec self#plain_copy_visitor spec)
+ register_new_components
+ (Cil.visitCilFunspec self#plain_copy_visitor spec)
| JustCopyPost f ->
- (register_new_components
- (Cil.visitCilFunspec self#plain_copy_visitor spec));
- ignore (f spec)
+ (register_new_components
+ (Cil.visitCilFunspec self#plain_copy_visitor spec));
+ ignore (f spec)
| DoChildren -> ignore (do_children ())
| DoChildrenPost f -> ignore (f (do_children ()))
| ChangeDoChildrenPost(spec, f) ->
- let res = change_do_children spec in
- register_new_components res;
- ignore (f res)
-
- method! vglob g =
- let fundec, has_kf = match g with
- | GFunDecl(_,v,_) ->
- let ov = Visitor_behavior.Get_orig.varinfo self#behavior v in
- let kf = try Globals.Functions.get ov with Not_found ->
- Kernel.fatal "No kernel function for %s(%d)" v.vname v.vid
- in
- (* Just make a copy of current kernel function in case it is needed *)
- let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
- if Visitor_behavior.is_copy self#behavior then
- new_kf.spec <- Cil.empty_funspec ();
- self#set_current_kf kf;
- None, true
- | GFun(f,_) ->
- let v = Visitor_behavior.Get_orig.varinfo self#behavior f.svar in
- let kf =
- try Globals.Functions.get v
- with Not_found ->
- Kernel.fatal "Visitor does not find function %s in %a"
- v.vname
- Project.pretty (Project.current ())
- in
- let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
- if Visitor_behavior.is_copy self#behavior then
- new_kf.spec <- Cil.empty_funspec ();
- self#set_current_kf kf;
- Some f, true
- | _ -> None, false
- in
- let res = self#vglob_aux g in
- let make_funspec () = match g with
- | GFunDecl _ | GFun _ when Ast.is_def_or_last_decl g ->
+ let res = change_do_children spec in
+ register_new_components res;
+ ignore (f res)
+
+ method! vglob g =
+ let fundec, has_kf = match g with
+ | GFunDecl(_,v,_) ->
+ let ov = Visitor_behavior.Get_orig.varinfo self#behavior v in
+ let kf = try Globals.Functions.get ov with Not_found ->
+ Kernel.fatal "No kernel function for %s(%d)" v.vname v.vid
+ in
+ (* Just make a copy of current kernel function in case it is needed *)
+ let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
+ if Visitor_behavior.is_copy self#behavior then
+ new_kf.spec <- Cil.empty_funspec ();
+ self#set_current_kf kf;
+ None, true
+ | GFun(f,_) ->
+ let v = Visitor_behavior.Get_orig.varinfo self#behavior f.svar in
+ let kf =
+ try Globals.Functions.get v
+ with Not_found ->
+ Kernel.fatal "Visitor does not find function %s in %a"
+ v.vname
+ Project.pretty (Project.current ())
+ in
+ let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
+ if Visitor_behavior.is_copy self#behavior then
+ new_kf.spec <- Cil.empty_funspec ();
+ self#set_current_kf kf;
+ Some f, true
+ | _ -> None, false
+ in
+ let res = self#vglob_aux g in
+ let make_funspec () = match g with
+ | GFunDecl _ | GFun _ when Ast.is_def_or_last_decl g ->
self#vfunspec_annot ();
- | _ -> ()
- in
- (* NB: we'll loose track of the emitter of an annotation.
- Anyway, this is only used for SkipChildren and JustCopy/JustCopyPost
- (and for a copy visitor)
- If user sticks to DoChildren, s/he'll still have the proper
- correspondence between annotations and emitters.
- *)
- let get_spec () = match g with
- | GFun _ | GFunDecl _ when Ast.is_def_or_last_decl g ->
- let spec =
- Annotations.funspec ~populate:false (Extlib.the self#current_kf)
- in
- Some (Cil.visitCilFunspec self#plain_copy_visitor spec)
- | _ -> None
- in
- let change_glob ng spec =
- let cond = Visitor_behavior.is_copy self#behavior in
- match ng with
+ | _ -> ()
+ in
+ (* NB: we'll loose track of the emitter of an annotation.
+ Anyway, this is only used for SkipChildren and JustCopy/JustCopyPost
+ (and for a copy visitor)
+ If user sticks to DoChildren, s/he'll still have the proper
+ correspondence between annotations and emitters.
+ *)
+ let get_spec () = match g with
+ | GFun _ | GFunDecl _ when Ast.is_def_or_last_decl g ->
+ let spec =
+ Annotations.funspec ~populate:false (Extlib.the self#current_kf)
+ in
+ Some (Cil.visitCilFunspec self#plain_copy_visitor spec)
+ | _ -> None
+ in
+ let change_glob ng spec =
+ let cond = Visitor_behavior.is_copy self#behavior in
+ match ng with
| GVar(vi,init,_) ->
- if cond then
- Queue.add
- (fun () ->
- try
- Globals.Vars.add vi init
- with Globals.Vars.AlreadyExists (vi,_) ->
- Kernel.fatal
- "Visitor is trying to insert global variable %a that \
- already exists in current project"
- Cil_datatype.Varinfo.pretty vi)
- self#get_filling_actions
+ if cond then
+ Queue.add
+ (fun () ->
+ try
+ Globals.Vars.add vi init
+ with Globals.Vars.AlreadyExists (vi,_) ->
+ Kernel.fatal
+ "Visitor is trying to insert global variable %a that \
+ already exists in current project"
+ Cil_datatype.Varinfo.pretty vi)
+ self#get_filling_actions
| GFunDecl(_,v,l) ->
- (match self#current_kf with
- | Some kf ->
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- if cond then begin
- Queue.add
- (fun () ->
- if Cil.hasAttribute "FC_BUILTIN" v.vattr then
- Cil.Frama_c_builtins.add v.vname v;
- if Cil_datatype.Varinfo.equal v
- (Kernel_function.get_vi new_kf)
- then begin
- let dft =
- Annotations.funspec ~populate:false new_kf
- in
- let dft =
- { dft with spec_behavior = dft.spec_behavior }
- in
- let spec = Extlib.opt_conv dft spec in
- Globals.Functions.register new_kf;
- Globals.Functions.replace_by_declaration spec v l;
+ (match self#current_kf with
+ | Some kf ->
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ if cond then begin
+ Queue.add
+ (fun () ->
+ if Cil.hasAttribute "FC_BUILTIN" v.vattr then
+ Cil.Frama_c_builtins.add v.vname v;
+ if Cil_datatype.Varinfo.equal v
+ (Kernel_function.get_vi new_kf)
+ then begin
+ let dft =
+ Annotations.funspec ~populate:false new_kf
+ in
+ let dft =
+ { dft with spec_behavior = dft.spec_behavior }
+ in
+ let spec = Extlib.opt_conv dft spec in
+ Globals.Functions.register new_kf;
+ Globals.Functions.replace_by_declaration spec v l;
(* Format.printf "registered spec:@\n%a@." Printer.pp_funspec
(Annotations.funspec ~populate:false new_kf) *)
- end else begin
- Globals.Functions.replace_by_declaration
- (Cil.empty_funspec()) v l
- end)
- self#get_filling_actions;
- if
- Cil_datatype.Varinfo.equal v
- (Kernel_function.get_vi new_kf) && Extlib.has_some spec
- then
- Queue.add
- (fun () ->
- Annotations.register_funspec ~force:true new_kf)
- self#get_filling_actions;
- end
- | None -> ()
- (* User is responsible for registering the new function *)
- )
- | GVarDecl (({vstorage=Extern} as v),_) (* when not (isFunctionType
- v.vtype) *) ->
- if cond then
- Queue.add
- (fun () ->
- try
- Globals.Vars.add_decl v
- with Globals.Vars.AlreadyExists (vi,_) ->
- Kernel.fatal
- "Visitor is trying to insert global variable %a that \
- already exists in current project"
- Cil_datatype.Varinfo.pretty vi)
- self#get_filling_actions
- | GFun(f,l) ->
- if cond then begin
- match self#current_kf with
+ end else begin
+ Globals.Functions.replace_by_declaration
+ (Cil.empty_funspec()) v l
+ end)
+ self#get_filling_actions;
+ if
+ Cil_datatype.Varinfo.equal v
+ (Kernel_function.get_vi new_kf) && Extlib.has_some spec
+ then
+ Queue.add
+ (fun () ->
+ Annotations.register_funspec ~force:true new_kf)
+ self#get_filling_actions;
+ end
+ | None -> ()
+ (* User is responsible for registering the new function *)
+ )
+ | GVarDecl (({vstorage=Extern} as v),_) (* when not (isFunctionType
+ v.vtype) *) ->
+ if cond then
+ Queue.add
+ (fun () ->
+ try
+ Globals.Vars.add_decl v
+ with Globals.Vars.AlreadyExists (vi,_) ->
+ Kernel.fatal
+ "Visitor is trying to insert global variable %a that \
+ already exists in current project"
+ Cil_datatype.Varinfo.pretty vi)
+ self#get_filling_actions
+ | GFun(f,l) ->
+ if cond then begin
+ match self#current_kf with
| Some kf ->
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ Queue.add
+ (fun () ->
+ Kernel.debug ~dkey:Kernel.dkey_visitor
+ "@[Adding definition %s (vid: %d) for project %s@\n\
+ body: %a@\n@]@."
+ f.svar.vname f.svar.vid
+ (Project.get_name (Project.current()))
+ Printer.pp_block f.sbody;
+ if cond && Cil.hasAttribute "FC_BUILTIN" f.svar.vattr then
+ Cil.Frama_c_builtins.add f.svar.vname f.svar;
+ if Cil_datatype.Varinfo.equal f.svar
+ (Kernel_function.get_vi new_kf)
+ then begin
+ Globals.Functions.register new_kf;
+ let spec =
+ Extlib.opt_conv
+ (Annotations.funspec ~populate:false new_kf) spec
+ in
+ Globals.Functions.replace_by_definition spec f l
+ end else
+ Globals.Functions.replace_by_definition
+ (Cil.empty_funspec ()) f l
+ )
+ self#get_filling_actions;
+ if Cil_datatype.Varinfo.equal f.svar
+ (Kernel_function.get_vi new_kf)
+ && Extlib.has_some spec
+ then
Queue.add
- (fun () ->
- Kernel.debug ~dkey:Kernel.dkey_visitor
- "@[Adding definition %s (vid: %d) for project %s@\n\
- body: %a@\n@]@."
- f.svar.vname f.svar.vid
- (Project.get_name (Project.current()))
- Printer.pp_block f.sbody;
- if cond && Cil.hasAttribute "FC_BUILTIN" f.svar.vattr then
- Cil.Frama_c_builtins.add f.svar.vname f.svar;
- if Cil_datatype.Varinfo.equal f.svar
- (Kernel_function.get_vi new_kf)
- then begin
- Globals.Functions.register new_kf;
- let spec =
- Extlib.opt_conv
- (Annotations.funspec ~populate:false new_kf) spec
- in
- Globals.Functions.replace_by_definition spec f l
- end else
- Globals.Functions.replace_by_definition
- (Cil.empty_funspec ()) f l
- )
+ (fun () -> Annotations.register_funspec ~force:true new_kf)
self#get_filling_actions;
- if Cil_datatype.Varinfo.equal f.svar
- (Kernel_function.get_vi new_kf)
- && Extlib.has_some spec
- then
- Queue.add
- (fun () -> Annotations.register_funspec ~force:true new_kf)
- self#get_filling_actions;
| None -> () (* User has to register the new function *)
- end
- | GAnnot (na,_) when cond ->
- let e = match g with
- | GAnnot (a,_) -> Annotations.emitter_of_global a
- | _ -> Emitter.end_user
- in
- Queue.add
- (fun () ->
- try
- (* Annotations might have already been added by the user. *)
- ignore (Annotations.emitter_of_global na)
- with Not_found ->
- Annotations.unsafe_add_global e na;
- )
- self#get_filling_actions
- | _ -> ()
- in
- let post_action g =
- Extlib.may self#set_current_func fundec;
- let spec = get_spec () in
- List.iter (fun g -> change_glob g spec) g;
- if has_kf then self#reset_current_kf();
- Extlib.may (fun _ -> self#reset_current_func ()) fundec;
- g
- in
- let post_change_to g =
- List.iter (fun g -> change_glob g None) g;
- if has_kf then self#reset_current_kf();
- g
- in
- let post_do_children f g =
- Extlib.may self#set_current_func fundec;
- make_funspec ();
- let res = f g in
- (* Spec registration is already handled at the vfunspec level. *)
- List.iter (fun g -> change_glob g None) res;
- if has_kf then self#reset_current_kf();
- Extlib.may (fun _ -> self#reset_current_func ()) fundec;
- res
- in
- match res with
- | SkipChildren ->
+ end
+ | GAnnot (na,_) when cond ->
+ let e = match g with
+ | GAnnot (a,_) -> Annotations.emitter_of_global a
+ | _ -> Emitter.end_user
+ in
+ Queue.add
+ (fun () ->
+ try
+ (* Annotations might have already been added by the user. *)
+ ignore (Annotations.emitter_of_global na)
+ with Not_found ->
+ Annotations.unsafe_add_global e na;
+ )
+ self#get_filling_actions
+ | _ -> ()
+ in
+ let post_action g =
+ Extlib.may self#set_current_func fundec;
+ let spec = get_spec () in
+ List.iter (fun g -> change_glob g spec) g;
+ if has_kf then self#reset_current_kf();
+ Extlib.may (fun _ -> self#reset_current_func ()) fundec;
+ g
+ in
+ let post_change_to g =
+ List.iter (fun g -> change_glob g None) g;
+ if has_kf then self#reset_current_kf();
+ g
+ in
+ let post_do_children f g =
+ Extlib.may self#set_current_func fundec;
+ make_funspec ();
+ let res = f g in
+ (* Spec registration is already handled at the vfunspec level. *)
+ List.iter (fun g -> change_glob g None) res;
+ if has_kf then self#reset_current_kf();
+ Extlib.may (fun _ -> self#reset_current_func ()) fundec;
+ res
+ in
+ match res with
+ | SkipChildren ->
change_glob g None;
if has_kf then self#reset_current_kf();
res
- | JustCopy -> JustCopyPost post_action
- | JustCopyPost f -> JustCopyPost (post_action $ f)
- | DoChildren -> DoChildrenPost (post_do_children Extlib.id)
- | DoChildrenPost f -> DoChildrenPost (post_do_children f)
- | ChangeTo l -> ChangeToPost (l,post_change_to)
- | ChangeToPost (l,f) -> ChangeToPost (l, post_change_to $ f)
- | ChangeDoChildrenPost (l,f) -> ChangeDoChildrenPost (l, post_do_children f)
-end
+ | JustCopy -> JustCopyPost post_action
+ | JustCopyPost f -> JustCopyPost (post_action $ f)
+ | DoChildren -> DoChildrenPost (post_do_children Extlib.id)
+ | DoChildrenPost f -> DoChildrenPost (post_do_children f)
+ | ChangeTo l -> ChangeToPost (l,post_change_to)
+ | ChangeToPost (l,f) -> ChangeToPost (l, post_change_to $ f)
+ | ChangeDoChildrenPost (l,f) -> ChangeDoChildrenPost (l, post_do_children f)
+ end
class generic_frama_c_visitor bhv =
let current_kf = ref None in
diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli
index 068752c85685180f4f8f09aa766bb2be482bf738..fc7803bc7e876e5217cb2259938b2f4aa2eb3bfb 100644
--- a/src/kernel_services/visitors/visitor.mli
+++ b/src/kernel_services/visitors/visitor.mli
@@ -35,69 +35,69 @@ open Cil_types
{b A few hints on how to use correctly this visitor}
- when initializing a new project with it
- (see {!File.init_project_from_visitor}), use a visitor with copy behavior
+ (see {!File.init_project_from_visitor}), use a visitor with copy behavior
- [SkipChildren] and [ChangeTo] must be used with extreme care in a visitor
- with copy behavior, or some nodes may be shared between the original and
- the copy.
+ with copy behavior, or some nodes may be shared between the original and
+ the copy.
- Do not erase a statement during the visit, as there might be
- annotations attached to it. Change it to Skip instead, the
- [generic_frama_c_visitor] will know what to do.
+ annotations attached to it. Change it to Skip instead, the
+ [generic_frama_c_visitor] will know what to do.
- Be careful if you change the [vid] or [sid]: this must be done before
- anything has been attached to the corresponding variable or
- statement in the new project, which means
- - for statements, in [vstmt], for the current statement only
- - for variables, at their declaration point. *)
+ anything has been attached to the corresponding variable or
+ statement in the new project, which means
+ -- for statements, in [vstmt], for the current statement only
+ -- for variables, at their declaration point. *)
class type frama_c_visitor = object
inherit Cil.cilVisitor
method frama_c_plain_copy: frama_c_visitor
- (** same as plain_copy_visitor but for frama-c specific methods *)
+ (** same as plain_copy_visitor but for frama-c specific methods *)
method vstmt_aux: stmt -> stmt Cil.visitAction
- (** Replacement of vstmt.
- @plugin development guide*)
+ (** Replacement of vstmt.
+ @plugin development guide*)
method vglob_aux: global -> global list Cil.visitAction
- (** Replacement of vglob.
- @plugin development guide*)
+ (** Replacement of vglob.
+ @plugin development guide*)
method current_kf: kernel_function option
- (** link to the kernel function currently being visited.
- {b NB:} for copy visitors, the link is to the original kf (anyway,
- the new kf is created only after the visit is over).
- @plugin development guide *)
+ (** link to the kernel function currently being visited.
+ {b NB:} for copy visitors, the link is to the original kf (anyway,
+ the new kf is created only after the visit is over).
+ @plugin development guide *)
method set_current_kf: kernel_function -> unit
- (** Internal use only. *)
+ (** Internal use only. *)
method reset_current_kf: unit -> unit
- (** Internal use only. *)
+ (** Internal use only. *)
end
class frama_c_inplace: frama_c_visitor
- (** in-place visitor; always act in the current project.
- @plugin development guide *)
+(** in-place visitor; always act in the current project.
+ @plugin development guide *)
class frama_c_copy: Project.t -> frama_c_visitor
- (** Copying visitor. The [Project.t] argument specifies in which project the
- visitor creates the new values. (Technically, the method
- [fill_global_tables] is called inside this project.)
- See {!File.init_project_from_visitor} and [create_project_from_visitor]
- for possible uses. *)
+(** Copying visitor. The [Project.t] argument specifies in which project the
+ visitor creates the new values. (Technically, the method
+ [fill_global_tables] is called inside this project.)
+ See {!File.init_project_from_visitor} and [create_project_from_visitor]
+ for possible uses. *)
class frama_c_refresh: Project.t -> frama_c_visitor
- (** Similar to {!frama_c_copy}, but ids will be refreshed in the copy.
- @since Sodium-20150201
- *)
+(** Similar to {!frama_c_copy}, but ids will be refreshed in the copy.
+ @since Sodium-20150201
+*)
class generic_frama_c_visitor:
Visitor_behavior.t -> frama_c_visitor
- (** Generic class that abstracts over [frama_c_inplace] and [frama_c_copy].
- @plugin development guide *)
+(** Generic class that abstracts over [frama_c_inplace] and [frama_c_copy].
+ @plugin development guide *)
(** Visit a file. This will re-cons all globals TWICE (so that it is
tail-recursive). Use {!Cil.visitCilFileSameGlobals} if your visitor will
@@ -111,21 +111,21 @@ val visitFramacFile: frama_c_visitor -> file -> unit
(** A visitor for the whole file that does not change the globals (but maybe
changes things inside the globals). Use this function instead of
{!Visitor.visitFramacFile} whenever appropriate because it is more
- efficient for long files.
+ efficient for long files.
@plugin development guide *)
val visitFramacFileSameGlobals: frama_c_visitor -> file -> unit
(** Visit a global.
-{b Warning} Do not call this function during another visit using the
-same visitor, as it is not reentrant: the inner visit will leave the visitor
-in an inconsistent state for the outer visit.
+ {b Warning} Do not call this function during another visit using the
+ same visitor, as it is not reentrant: the inner visit will leave the visitor
+ in an inconsistent state for the outer visit.
*)
val visitFramacGlobal: frama_c_visitor -> global -> global list
(** Visit a kernel_function. More precisely, the entry point for the visit
will be the global corresponding to the last declaration/definition of
- the kf. The returned kf is the one that has the varinfo
+ the kf. The returned kf is the one that has the varinfo
associated to the varinfo of the original kf. If this is a new kf, it is
however the responsibility of the visitor to insert it in the AST at
the appropriate place.
@@ -165,7 +165,7 @@ val visitFramacType: frama_c_visitor -> typ -> typ
(** Visit a variable declaration *)
val visitFramacVarDecl: frama_c_visitor -> varinfo -> varinfo
-(** Visit a logic variable declaration
+(** Visit a logic variable declaration
@since Magnesium-20151001
*)
@@ -209,7 +209,7 @@ val visitFramacPredicates: frama_c_visitor -> identified_predicate list
(** visit identified_term.
@since Oxygen-20120901
- *)
+*)
val visitFramacIdTerm: frama_c_visitor -> identified_term -> identified_term
val visitFramacTerm: frama_c_visitor -> term -> term
diff --git a/src/plugins/gui/filetree.mli b/src/plugins/gui/filetree.mli
index 0cce6d677ca3f3f1f865c35ec23fbbd4eaa7e7be..bf353c76894432e5de4c568bd0bf29869aeb681b 100644
--- a/src/plugins/gui/filetree.mli
+++ b/src/plugins/gui/filetree.mli
@@ -25,70 +25,71 @@
type filetree_node =
| File of Datatype.Filepath.t * Cil_types.global list
| Global of Cil_types.global
-(** Caml type for the infos on a node of the tree. Not all globals appear
- in the filetree. Currently, the visible ones are:
- - functions definitions, or declarations if no definition exists
- - global variables
- - global annotations
- @since Nitrogen-20111001 *)
+ (** Caml type for the infos on a node of the tree. Not all globals appear
+ in the filetree. Currently, the visible ones are:
+ - functions definitions, or declarations if no definition exists
+ - global variables
+ - global annotations
+
+ @since Nitrogen-20111001 *)
class type t = object
method model : GTree.model
method flat_mode: bool
- (** Return [true] if the filetree currently displays all globals in
- flat mode (all children of the same node), [false] otherwise
- (children of the file they are declared in). If [true], the methods
- [set_file_attribute] and [get_files_globals] must not be used
+ (** Return [true] if the filetree currently displays all globals in
+ flat mode (all children of the same node), [false] otherwise
+ (children of the file they are declared in). If [true], the methods
+ [set_file_attribute] and [get_files_globals] must not be used
- @since Nitrogen-20111001 *)
+ @since Nitrogen-20111001 *)
method set_file_attribute:
?strikethrough:bool -> ?text:string -> Datatype.Filepath.t -> unit
- (** Manually set some attributes of the given filename. *)
+ (** Manually set some attributes of the given filename. *)
method set_global_attribute:
?strikethrough:bool -> ?text:string -> Cil_types.varinfo -> unit
- (** Manually set some attributes of the given variable. *)
+ (** Manually set some attributes of the given variable. *)
method add_global_filter:
text:string ->
key:string ->
(Cil_types.global -> bool) ->
(unit -> bool) * GMenu.check_menu_item
- (** [add_global_filter text key f] adds a filter for the visibility of
- the globals, according to [f]. If any of the filters registered
- through this method returns true, the global is not displayed in the
- filetree. [text] is used in the filetree menu, to label the entry
- permitting to activate or deactivate the filter. [key] is used to
- store the current state of the filter internally. The created
- menu is returned.
-
- @since Nitrogen-20111001
- @modify Oxygen-20120901 Signature change for the filter argument,
- return the menu.
- *)
+ (** [add_global_filter text key f] adds a filter for the visibility of
+ the globals, according to [f]. If any of the filters registered
+ through this method returns true, the global is not displayed in the
+ filetree. [text] is used in the filetree menu, to label the entry
+ permitting to activate or deactivate the filter. [key] is used to
+ store the current state of the filter internally. The created
+ menu is returned.
+
+ @since Nitrogen-20111001
+ @modify Oxygen-20120901 Signature change for the filter argument,
+ return the menu.
+ *)
method get_file_globals:
Datatype.Filepath.t -> (string * bool) list
- (** Return the names and the attributes (currently only the strikethrough
- property) of the globals in the file passed as argument *)
+ (** Return the names and the attributes (currently only the strikethrough
+ property) of the globals in the file passed as argument *)
method find_visible_global:
string -> Cil_types.global option
- (** [find_visible_global str] searches for the next occurrence of a visible
- global whose name contains [str], starting at the currently selected
- element. Returns the global found (if any).
+ (** [find_visible_global str] searches for the next occurrence of a visible
+ global whose name contains [str], starting at the currently selected
+ element. Returns the global found (if any).
- @since Magnesium-20151001 *)
+ @since Magnesium-20151001 *)
method add_select_function :
(was_activated:bool -> activating:bool -> filetree_node -> unit) -> unit
- (** Register a callback that is called whenever an element of the file tree
- is selected or unselected.
+ (** Register a callback that is called whenever an element of the file tree
+ is selected or unselected.
- @modify Nitrogen-20111001 Changed argument from a list
- of globals to [filetree_node] *)
+ @modify Nitrogen-20111001 Changed argument from a list
+ of globals to [filetree_node] *)
method append_text_column:
title:string ->
@@ -137,27 +138,27 @@ class type t = object
a [varinfo]. Returns a boolean to indicate success or failure. *)
method selected_globals : Cil_types.global list
- (** @since Carbon-20101201
- @return the list of selected globals in the treeview. *)
+ (** @since Carbon-20101201
+ @return the list of selected globals in the treeview. *)
method view : GTree.view
- (** The tree view associated in which the file tree is packed. *)
+ (** The tree view associated in which the file tree is packed. *)
method reset : unit -> unit
- (** Resynchronize the tree view with the current project state.
- This is called in particular by the generic reset extension of
- {!Design} *)
+ (** Resynchronize the tree view with the current project state.
+ This is called in particular by the generic reset extension of
+ {!Design} *)
method register_reset_extension : (t -> unit) -> unit
(** Register a function to be called whenever the reset method of the
filetree is called. *)
method refresh_columns : unit -> unit
- (** Refresh the state of all the non-source columns of the filetree,
- by hiding those that should be hidden, and displaying the
- others. Called by [reset]
+ (** Refresh the state of all the non-source columns of the filetree,
+ by hiding those that should be hidden, and displaying the
+ others. Called by [reset]
- @since Nitrogen-20111001 *)
+ @since Nitrogen-20111001 *)
end
val make : GTree.view -> t
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index f39592a07eb42ec3a47de75bc6ac63ee797cdebc..8ffbbd33ffe88bb841978194009ac0059094a6e5 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -34,7 +34,7 @@ let html_stag_functions =
let index = String.index t ' ' in
Format.sprintf "</%s>" (String.sub t 0 index)
with
- | Not_found -> Format.sprintf "</%s>" t
+ | Not_found -> Format.sprintf "</%s>" t
and print_open_stag _ = ()
and print_close_stag _ = ()
in
@@ -64,7 +64,7 @@ module OptionKf =
(** Defining base metrics and operations on those *)
module BasicMetrics = struct
-(** Record type to compute cyclomatic complexity *)
+ (** Record type to compute cyclomatic complexity *)
type t = {
cfile_name : Datatype.Filepath.t;
@@ -139,11 +139,11 @@ module BasicMetrics = struct
;;
let labels =
- [ "Sloc"; "Decision point"; "Global variables"; "If"; "Loop"; "Goto";
- "Assignment"; "Exit point"; "Function"; "Function call";
- "Pointer dereferencing";
- "Cyclomatic complexity";
- ]
+ [ "Sloc"; "Decision point"; "Global variables"; "If"; "Loop"; "Goto";
+ "Assignment"; "Exit point"; "Function"; "Function call";
+ "Pointer dereferencing";
+ "Cyclomatic complexity";
+ ]
;;
let str_values metrics =
@@ -162,12 +162,12 @@ module BasicMetrics = struct
let pp_func_or_none =
Pretty_utils.pp_opt ~none:"<none>" Kernel_function.pretty
-(* Pretty print metrics as text eg. in stdout *)
+ (* Pretty print metrics as text eg. in stdout *)
let pp_base_metrics fmt metrics =
let heading =
if metrics.cfile_name = Datatype.Filepath.dummy &&
metrics.cfunc = None then
- (* It is a global metrics *)
+ (* It is a global metrics *)
"Global metrics"
else
Format.asprintf "Stats for function <%a/%a>"
@@ -177,12 +177,12 @@ module BasicMetrics = struct
Format.fprintf fmt "@[<v 0>%a @ %a@]"
(mk_hdr 1) heading
((fun l1 ppf l2 ->
- List.iter2 (fun x y -> Format.fprintf ppf "%s = %s@ " x y)
- l1 l2) labels)
+ List.iter2 (fun x y -> Format.fprintf ppf "%s = %s@ " x y)
+ l1 l2) labels)
(str_values metrics)
;;
-(* Dummy utility functions for pretty printing simple types *)
+ (* Dummy utility functions for pretty printing simple types *)
let pp_int fmt n = Format.fprintf fmt "%d" n
;;
@@ -242,7 +242,7 @@ let get_suffix filename =
String.sub filename (succ last_dot_idx) (slen - last_dot_idx - 1)
else ""
with
- | Not_found -> raise No_suffix
+ | Not_found -> raise No_suffix
;;
type output_type =
@@ -254,16 +254,16 @@ type output_type =
let get_file_type filename =
try
match get_suffix filename with
- | "html" | "htm" -> Html
- | "txt" | "text" -> Text
- | "json" -> Json
- | s ->
- Metrics_parameters.abort
- "Unknown file extension %s. Cannot produce output.@." s
+ | "html" | "htm" -> Html
+ | "txt" | "text" -> Text
+ | "json" -> Json
+ | s ->
+ Metrics_parameters.abort
+ "Unknown file extension %s. Cannot produce output.@." s
with
- | No_suffix ->
- Metrics_parameters.abort
- "File %s has no suffix. Cannot produce output.@." filename
+ | No_suffix ->
+ Metrics_parameters.abort
+ "File %s has no suffix. Cannot produce output.@." filename
module VarinfoByName = struct
type t = Cil_types.varinfo
@@ -280,10 +280,10 @@ let pretty_set fmt s =
Format.fprintf fmt "@[";
VInfoMap.iter
(fun f n ->
- Format.fprintf fmt "%s %s(%d call%s);@ "
- f.Cil_types.vname
- (if f.vaddrof then "(address taken) " else "")
- n (if n > 1 then "s" else ""))
+ Format.fprintf fmt "%s %s(%d call%s);@ "
+ f.Cil_types.vname
+ (if f.vaddrof then "(address taken) " else "")
+ n (if n > 1 then "s" else ""))
s;
Format.fprintf fmt "@]"
@@ -318,8 +318,8 @@ let pretty_entry_points fmt fs =
let print fmt =
VInfoMap.iter
(fun fvinfo n ->
- if is_entry_point fvinfo n
- then Format.fprintf fmt "%s;@ " fvinfo.vname)
+ if is_entry_point fvinfo n
+ then Format.fprintf fmt "%s;@ " fvinfo.vname)
in
Format.fprintf fmt "@[<hov 1>%a@]" print fs;
;;
@@ -339,7 +339,7 @@ let json_of_entry_points m =
let file_of_vinfodef fvinfo =
let kf = Globals.Functions.get fvinfo in
let decl_loc1, _decl_loc2 =
- match kf.fundec with
+ match kf.fundec with
| Definition (_, loc) -> loc
| Declaration (_, _, _, loc) -> loc
in decl_loc1.Filepath.pos_path
@@ -353,12 +353,12 @@ let file_of_fundef (fun_dec: Cil_types.fundec) =
let extract_fundef_name sname =
match sname with
- | _spec, (the_name, _, _, _) -> the_name
+ | _spec, (the_name, _, _, _) -> the_name
;;
let kf_of_cabs_name sname =
match sname with
- | _spec, (the_name, _, _, _) -> Globals.Functions.find_by_name the_name
+ | _spec, (the_name, _, _, _) -> Globals.Functions.find_by_name the_name
let get_filename fdef =
match fdef with
@@ -371,11 +371,11 @@ let consider_function ~libc vinfo =
not (!Db.Value.mem_builtin vinfo.vname
|| Ast_info.is_frama_c_builtin vinfo.vname
|| Cil.is_unused_builtin vinfo
- ) && (libc || not (is_in_libc vinfo.vattr))
+ ) && (libc || not (is_in_libc vinfo.vattr))
let consider_variable ~libc vinfo =
not (Cil.hasAttribute "FRAMA_C_MODEL" vinfo.vattr) &&
- (libc || not (is_in_libc vinfo.vattr))
+ (libc || not (is_in_libc vinfo.vattr))
let float_to_string f =
let s = Format.sprintf "%F" f in
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index 1b209bbd078e665182942b0bba4e0c18d96e3e21..6e4b361b7bfa7c4b5d26e0234ff54b1973211aea 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -29,6 +29,7 @@ val html_stag_functions : Format.formatter_stag_functions;;
- level 1 headers are underlined by '='
- level 2 headers by '-'
- level 3 headers by '~'
+
This function is supposed to follow reStructuredText's conventions.
*)
val mk_hdr : int -> Format.formatter -> string -> unit;;
@@ -52,7 +53,7 @@ module BasicMetrics : sig
function, possibly more for a file.*)
cptrs: int ; (** Access to pointers *)
cdecision_points: int ; (** Decision points of the program: ifs,
- switch cases, exception handlers, ... *)
+ switch cases, exception handlers, ... *)
cglob_vars: int; (** Global variables *)
ccyclo: int; (** Cyclomatic complexity *)
}
@@ -164,7 +165,7 @@ val consider_variable: libc:bool -> Cil_types.varinfo -> bool
(** Convert float to string with the following convention:
- if the float is an integer (ie, it has no digits after the decimal point),
- print it as such;
+ print it as such;
- otherwise, print the first two digits after the decimal point.
*)
val float_to_string : float -> string ;;
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 6647c539acf0696c7c8f7f84eda30496e9ffe98f..4b9833f5baa59920c4c73f3f73ef3bbbbccc9d0c 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -85,17 +85,17 @@ module V = struct
let is_imprecise v =
match v with
- | Top _ -> true
- | _ -> false
+ | Top _ -> true
+ | _ -> false
- let is_topint v = equal top_int v
+ let is_topint v = equal top_int v
let is_bottom v = equal bottom v
let is_isotropic v =
match v with
- | Top _ -> true
- | Map _ -> is_topint v || is_bottom v || is_zero v
+ | Top _ -> true
+ | Map _ -> is_topint v || is_bottom v || is_zero v
let contains_zero loc =
let offset_contains_zero base offset =
@@ -271,17 +271,17 @@ module V = struct
let backward_rel_int_left op l r =
let open Abstract_interp.Comp in
match l with
- | Top _ -> l
- | Map m1 ->
- try
- let k,v2 = find_lonely_key r in
- let v1 = find_or_bottom k m1 in
- let v1' = Ival.backward_comp_int_left op v1 v2 in
- let r = add k v1' l in
- if (not (Base.equal k Base.null)) && (op = Ge || op = Gt)
- then diff_if_one r singleton_zero
- else r
- with Not_found -> l
+ | Top _ -> l
+ | Map m1 ->
+ try
+ let k,v2 = find_lonely_key r in
+ let v1 = find_or_bottom k m1 in
+ let v1' = Ival.backward_comp_int_left op v1 v2 in
+ let r = add k v1' l in
+ if (not (Base.equal k Base.null)) && (op = Ge || op = Gt)
+ then diff_if_one r singleton_zero
+ else r
+ with Not_found -> l
(* More aggressive reduction by relational pointer operators. This version
assumes that \pointer_comparable alarms have been emitted, and that
@@ -313,8 +313,8 @@ module V = struct
(* i1' and p1' are pointwise application of the comparison operator,
and will be in the result in all cases. *)
if debug then Kernel.result "%a %a %a %a %a -> %a %a"
- Ival.pretty il pretty pl pretty_comp op Ival.pretty ir pretty pr
- Ival.pretty il' pretty pl';
+ Ival.pretty il pretty pl pretty_comp op Ival.pretty ir pretty pr
+ Ival.pretty il' pretty pl';
match op, zl, zr with
| (Le | Lt), false, _ (* il + pl <~ (ir + ?0) + pr *)
| (Ge | Gt), _, false (* (il + ?0) + pl >~ ir + pr *) ->
@@ -375,10 +375,10 @@ module V = struct
|| (e2_zero && (op = Ge || op = Gt))
then True (* if e1/e2 is NULL, then e2/e1 is a pointer *)
else
- if (e2_zero && (op = Le || op = Lt))
- || (e1_zero && (op = Ge || op = Gt))
- then False
- else Unknown
+ if (e2_zero && (op = Le || op = Lt))
+ || (e1_zero && (op = Ge || op = Gt))
+ then False
+ else Unknown
end
end
with Not_found -> Comp.Unknown
@@ -393,9 +393,9 @@ module V = struct
let forward_comp_int ~signed op v1 v2 =
let open Abstract_interp.Comp in
match op with
- | Eq -> forward_eq_int v1 v2
- | Ne -> inv_truth (forward_eq_int v1 v2)
- | Le | Ge | Lt | Gt -> forward_rel_int ~signed op v1 v2
+ | Eq -> forward_eq_int v1 v2
+ | Ne -> inv_truth (forward_eq_int v1 v2)
+ | Le | Ge | Lt | Gt -> forward_rel_int ~signed op v1 v2
(** Casts and reinterpretation *)
@@ -428,9 +428,9 @@ module V = struct
(* ok_garbled indicates that we do _not_ create a (new) garbled mix *)
let pointer_part', ok_garbled =
if Int.ge size (Int.of_int (Bit_utils.sizeofpointer ())) ||
- is_bottom pointer_part || is_imprecise pointer_part
+ is_bottom pointer_part || is_imprecise pointer_part
then pointer_part, true
- else topify_arith_origin pointer_part, false
+ else topify_arith_origin pointer_part, false
in
if ok_garbled && integer_part' == integer_part then
v (* both pointer and integer part are unchanged *)
@@ -444,38 +444,38 @@ module V = struct
to_int Ival.reinterpret_as_int ~size ~signed v
let cast_float_to_int ~signed ~size v =
- try
- let v1 = project_ival v in
- let r = Ival.cast_float_to_int ~signed ~size v1 in
- inject_ival r
- with Not_based_on_null ->
- if is_bottom v
- then v
- else topify_arith_origin v
-
- let cast_float_to_int_inverse ~single_precision i =
- try
- let v1 = project_ival i in
- let r = Ival.cast_float_to_int_inverse ~single_precision v1 in
- Some (inject_ival r)
- with Not_based_on_null -> None
-
- let cast_int_to_float kind v =
- try
- let i = project_ival v in
- let r = Ival.cast_int_to_float kind i in
- inject_ival r
- with Not_based_on_null ->
- if is_bottom v
- then bottom
- else topify_arith_origin v
-
- let cast_int_to_float_inverse ~single_precision vf =
- try
- let ivf = project_ival vf in
- let i = Ival.cast_int_to_float_inverse ~single_precision ivf in
- Some (inject_ival i)
- with Not_based_on_null -> None
+ try
+ let v1 = project_ival v in
+ let r = Ival.cast_float_to_int ~signed ~size v1 in
+ inject_ival r
+ with Not_based_on_null ->
+ if is_bottom v
+ then v
+ else topify_arith_origin v
+
+ let cast_float_to_int_inverse ~single_precision i =
+ try
+ let v1 = project_ival i in
+ let r = Ival.cast_float_to_int_inverse ~single_precision v1 in
+ Some (inject_ival r)
+ with Not_based_on_null -> None
+
+ let cast_int_to_float kind v =
+ try
+ let i = project_ival v in
+ let r = Ival.cast_int_to_float kind i in
+ inject_ival r
+ with Not_based_on_null ->
+ if is_bottom v
+ then bottom
+ else topify_arith_origin v
+
+ let cast_int_to_float_inverse ~single_precision vf =
+ try
+ let ivf = project_ival vf in
+ let i = Ival.cast_int_to_float_inverse ~single_precision ivf in
+ Some (inject_ival i)
+ with Not_based_on_null -> None
(** Binary functions *)
@@ -485,13 +485,13 @@ module V = struct
let v2 = project_ival e2 in
inject_ival (f v1 v2)
with Not_based_on_null ->
- if is_bottom e1 || is_bottom e2
+ if is_bottom e1 || is_bottom e2
then bottom
else begin
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
- end
+ join
+ (topify_with_origin_kind topify e1)
+ (topify_with_origin_kind topify e2)
+ end
let arithmetic_function = import_function ~topify:Origin.K_Arith
@@ -520,23 +520,23 @@ module V = struct
try
Location_Bytes.shift (project_ival_bottom e2) e1
with Not_based_on_null ->
- try (* On the off chance that someone writes [i+(int)&p]... *)
- Location_Bytes.shift (project_ival_bottom e1) e2
- with Not_based_on_null ->
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ try (* On the off chance that someone writes [i+(int)&p]... *)
+ Location_Bytes.shift (project_ival_bottom e1) e2
+ with Not_based_on_null ->
+ join
+ (topify_with_origin_kind topify e1)
+ (topify_with_origin_kind topify e2)
end
with Not_found ->
- (* we end up here if the only way left to make this
- addition is to convert e2 to an integer *)
- try
- let right = Ival.scale_int_base factor (project_ival_bottom e2)
- in Location_Bytes.shift right e1
- with Not_based_on_null -> (* from [project_ival] *)
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ (* we end up here if the only way left to make this
+ addition is to convert e2 to an integer *)
+ try
+ let right = Ival.scale_int_base factor (project_ival_bottom e2)
+ in Location_Bytes.shift right e1
+ with Not_based_on_null -> (* from [project_ival] *)
+ join
+ (topify_with_origin_kind topify e1)
+ (topify_with_origin_kind topify e2)
(* Under-approximating variant of add_untyped. Takes two
under-approximation, and returns an under-approximation.*)
@@ -544,13 +544,13 @@ module V = struct
if Int_Base.equal factor (Int_Base.minus_one)
then
(* Note: we could do a "link" for each pair of matching bases in
- e1 and e2, so this is an underapproximation in the most
- common case. *)
+ e1 and e2, so this is an underapproximation in the most
+ common case. *)
try
- let b1, o1 = Location_Bytes.find_lonely_key e1 in
- let b2, o2 = Location_Bytes.find_lonely_key e2 in
- if Base.compare b1 b2 <> 0 then bottom
- else inject_ival (Ival.sub_int_under o1 o2)
+ let b1, o1 = Location_Bytes.find_lonely_key e1 in
+ let b2, o2 = Location_Bytes.find_lonely_key e2 in
+ if Base.compare b1 b2 <> 0 then bottom
+ else inject_ival (Ival.sub_int_under o1 o2)
with Not_found -> bottom
else if Int_Base.equal factor Int_Base.one
then
@@ -558,8 +558,8 @@ module V = struct
with Not_based_on_null -> bottom
else
try
- let right = Ival.scale_int_base factor (project_ival_bottom e2) in
- Location_Bytes.shift_under right e1
+ let right = Ival.scale_int_base factor (project_ival_bottom e2) in
+ Location_Bytes.shift_under right e1
with Not_based_on_null -> bottom
;;
@@ -648,14 +648,14 @@ module V = struct
let merge_distinct_bits ~topify ~conflate_bottom value acc =
if is_bottom acc || is_bottom value
then begin
- if conflate_bottom
- then
- bottom
- else
- join
- (topify_with_origin_kind topify acc)
- (topify_with_origin_kind topify value)
- end
+ if conflate_bottom
+ then
+ bottom
+ else
+ join
+ (topify_with_origin_kind topify acc)
+ (topify_with_origin_kind topify value)
+ end
else
add_untyped ~topify ~factor:Int_Base.one value acc
@@ -668,7 +668,7 @@ module V = struct
try
let i = project_ival v in
Ival.all_values ~size i
- with Not_based_on_null ->
+ with Not_based_on_null ->
false
let anisotropic_cast ~size v =
@@ -690,7 +690,7 @@ module V = struct
let add_untyped ~factor v1 v2 =
add_untyped ~topify:Origin.K_Arith ~factor v1 v2
-
+
end
module V_Or_Uninitialized = struct
@@ -706,10 +706,10 @@ module V_Or_Uninitialized = struct
let make ~initialized ~escaping v =
match initialized, escaping with
- | true, false -> C_init_noesc v
- | true, true -> C_init_esc v
- | false, false -> C_uninit_noesc v
- | false, true -> C_uninit_esc v
+ | true, false -> C_init_noesc v
+ | true, true -> C_init_esc v
+ | false, false -> C_uninit_noesc v
+ | false, true -> C_uninit_esc v
let mask_init = 2
let mask_noesc = 1
@@ -719,7 +719,7 @@ module V_Or_Uninitialized = struct
let is_initialized v = (get_flags v land mask_init) <> 0
let is_noesc v = (get_flags v land mask_noesc) <> 0
- let get_v = function
+ let get_v = function
| C_uninit_esc v
| C_uninit_noesc v
| C_init_esc v
@@ -737,7 +737,7 @@ module V_Or_Uninitialized = struct
| 3 -> C_init_noesc v
| _ -> assert false
-(* let (==>) = (fun x y -> (not x) || y) *)
+ (* let (==>) = (fun x y -> (not x) || y) *)
type size_widen_hint = V.size_widen_hint
type numerical_widen_hint = V.numerical_widen_hint
@@ -765,7 +765,7 @@ module V_Or_Uninitialized = struct
(V.link (get_v t1) (get_v t2))
let meet t1 t2 =
- create
+ create
((get_flags t1) lor (get_flags t2))
(V.meet (get_v t1) (get_v t2))
@@ -783,36 +783,36 @@ module V_Or_Uninitialized = struct
let initialized v = C_init_noesc v
let is_included t1 t2 =
-(* (t2.initialized ==> t1.initialized) &&
- (t2.no_escaping_adr ==> t1.no_escaping_adr) &&
- V.is_included t1.v t2.v
-*)
+ (* (t2.initialized ==> t1.initialized) &&
+ (t2.no_escaping_adr ==> t1.no_escaping_adr) &&
+ V.is_included t1.v t2.v
+ *)
let flags1 = get_flags t1 in
let flags2 = get_flags t2 in
(lnot flags2) lor flags1 = -1 &&
- V.is_included (get_v t1) (get_v t2)
+ V.is_included (get_v t1) (get_v t2)
let pretty_aux pp fmt t =
let no_escaping_adr = is_noesc t in
let initialized = is_initialized t in
let v = get_v t in
match V.(equal bottom v), initialized, no_escaping_adr with
- | false, false, false ->
- Format.fprintf fmt "%a or UNINITIALIZED or ESCAPINGADDR" pp v
- | true, false, false ->
- Format.pp_print_string fmt "UNINITIALIZED or ESCAPINGADDR"
- | false, false, true ->
- Format.fprintf fmt "%a or UNINITIALIZED" pp v
- | true, false, true ->
- Format.pp_print_string fmt "UNINITIALIZED"
- | false, true, false ->
- Format.fprintf fmt "%a or ESCAPINGADDR" pp v
- | true, true, false ->
- Format.pp_print_string fmt "ESCAPINGADDR"
- | false, true, true ->
- pp fmt v
- | true, true, true ->
- Format.pp_print_string fmt "BOTVALUE"
+ | false, false, false ->
+ Format.fprintf fmt "%a or UNINITIALIZED or ESCAPINGADDR" pp v
+ | true, false, false ->
+ Format.pp_print_string fmt "UNINITIALIZED or ESCAPINGADDR"
+ | false, false, true ->
+ Format.fprintf fmt "%a or UNINITIALIZED" pp v
+ | true, false, true ->
+ Format.pp_print_string fmt "UNINITIALIZED"
+ | false, true, false ->
+ Format.fprintf fmt "%a or ESCAPINGADDR" pp v
+ | true, true, false ->
+ Format.pp_print_string fmt "ESCAPINGADDR"
+ | false, true, true ->
+ pp fmt v
+ | true, true, true ->
+ Format.pp_print_string fmt "BOTVALUE"
let pretty fmt v = pretty_aux V.pretty fmt v
let pretty_typ typ fmt v =
@@ -828,38 +828,38 @@ module V_Or_Uninitialized = struct
include
(Datatype.Make
- (struct
- type uninitialized = t
- type t = uninitialized (* = | C_uninit_esc of V.t
- | C_uninit_noesc of V.t
- | C_init_esc of V.t
- | C_init_noesc of V.t *)
- let name = "Cvalue.V_Or_Uninitialized"
- let structural_descr =
- let v = V.packed_descr in
+ (struct
+ type uninitialized = t
+ type t = uninitialized (* = | C_uninit_esc of V.t
+ | C_uninit_noesc of V.t
+ | C_init_esc of V.t
+ | C_init_noesc of V.t *)
+ let name = "Cvalue.V_Or_Uninitialized"
+ let structural_descr =
+ let v = V.packed_descr in
Structural_descr.t_sum [| [| v |]; [| v |]; [| v |]; [| v |] |]
- let reprs =
- List.fold_left
- (fun acc v ->
- List.fold_left
- (fun acc v ->
- List.fold_left
- (fun acc v -> C_uninit_noesc v :: acc)
- (C_uninit_esc v :: acc)
- V.reprs)
- (C_init_noesc v :: acc)
- V.reprs)
- (List.map (fun v -> C_init_esc v) V.reprs)
- V.reprs
- let hash = hash
- let equal = equal
- let compare = Datatype.undefined
- let copy = Datatype.undefined
- let rehash = Datatype.identity
- let pretty = pretty
- let internal_pretty_code = Datatype.undefined
- let varname = Datatype.undefined
- let mem_project = Datatype.never_any_project
+ let reprs =
+ List.fold_left
+ (fun acc v ->
+ List.fold_left
+ (fun acc v ->
+ List.fold_left
+ (fun acc v -> C_uninit_noesc v :: acc)
+ (C_uninit_esc v :: acc)
+ V.reprs)
+ (C_init_noesc v :: acc)
+ V.reprs)
+ (List.map (fun v -> C_init_esc v) V.reprs)
+ V.reprs
+ let hash = hash
+ let equal = equal
+ let compare = Datatype.undefined
+ let copy = Datatype.undefined
+ let rehash = Datatype.identity
+ let pretty = pretty
+ let internal_pretty_code = Datatype.undefined
+ let varname = Datatype.undefined
+ let mem_project = Datatype.never_any_project
end)
: Datatype.S with type t := t)
@@ -998,7 +998,7 @@ module V_Offsetmap = struct
let narrow_reinterpret x y =
try `Value (OffsetmapNarrow.narrow_reinterpret x y)
with NarrowReturnsBottom -> `Bottom
-
+
end
module Default_offsetmap = struct
@@ -1007,10 +1007,10 @@ module Default_offsetmap = struct
State_builder.Int_hashtbl
(V_Offsetmap)
(struct
- let name = "Cvalue.Default_offsetmap.StringOffsetmaps"
- let dependencies = [ Ast.self ]
- let size = 17
- end)
+ let name = "Cvalue.Default_offsetmap.StringOffsetmaps"
+ let dependencies = [ Ast.self ]
+ let size = 17
+ end)
let () = Ast.add_monotonic_state StringOffsetmaps.self
let default_offsetmap base =
@@ -1046,7 +1046,7 @@ module Default_offsetmap = struct
sets of locals, but is is ok to have missing ones considered as being
bound to Bottom.
- for dynamic allocation, the default value is indeed Bottom
- *)
+ *)
let name = "Cvalue.Default_offsetmap"
@@ -1077,7 +1077,7 @@ module Model = struct
let reduce_indeterminate_binding state l v =
assert (Locations.cardinal_zero_or_one l);
add_binding ~exact:true state l v
-
+
(* Overwrites the definition of add_binding coming from Lmap, with a
signature change. *)
let add_binding ~exact acc loc value =
@@ -1087,18 +1087,18 @@ module Model = struct
List.fold_left
(fun acc block -> remove_variables block.blocals acc) state blocks
- let cardinal_estimate state =
- match state with
- | Bottom -> CardinalEstimate.zero
- | Top -> CardinalEstimate.infinite
- | Map(m) ->
- let count = ref (CardinalEstimate.one) in
- let f _ offsetmap =
- let offsetmap_card = V_Offsetmap.cardinal_estimate offsetmap in
- count := CardinalEstimate.mul !count offsetmap_card
- in
- iter f m;
- !count
+ let cardinal_estimate state =
+ match state with
+ | Bottom -> CardinalEstimate.zero
+ | Top -> CardinalEstimate.infinite
+ | Map(m) ->
+ let count = ref (CardinalEstimate.one) in
+ let f _ offsetmap =
+ let offsetmap_card = V_Offsetmap.cardinal_estimate offsetmap in
+ count := CardinalEstimate.mul !count offsetmap_card
+ in
+ iter f m;
+ !count
end
(*
diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli
index dc2f6ae7dd335273ae7014033fba9926c1cfb4e6..0b55de0ca3eea5e22593c6429141846bdc3f222e 100644
--- a/src/plugins/value_types/cvalue.mli
+++ b/src/plugins/value_types/cvalue.mli
@@ -26,7 +26,7 @@ open Abstract_interp
open Locations
(** Estimation of the cardinal of the concretization of an abstract state
- or value. *)
+ or value. *)
module CardinalEstimate: sig
type t
val one: t
@@ -45,15 +45,15 @@ module V : sig
(* Too many aliases, and OCaml module system is not able to keep track
of all of them. Use some shortcuts *)
with type M.t = Location_Bytes.M.t
- and type t = Location_Bytes.t
- and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
- and type size_widen_hint = Location_Bytes.size_widen_hint
+ and type t = Location_Bytes.t
+ and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
+ and type size_widen_hint = Location_Bytes.size_widen_hint
include module type of Offsetmap_lattice_with_isotropy
- with type t := t
- and type numerical_widen_hint := numerical_widen_hint
- and type size_widen_hint := size_widen_hint
- and type widen_hint := widen_hint
+ with type t := t
+ and type numerical_widen_hint := numerical_widen_hint
+ and type size_widen_hint := size_widen_hint
+ and type widen_hint := widen_hint
val pretty_typ: Cil_types.typ option -> t Pretty_utils.formatter
@@ -69,7 +69,7 @@ module V : sig
val project_ival_bottom: t -> Ival.t
(* Temporary API, will be merged with project_ival later *)
-
+
val is_imprecise : t -> bool
val is_topint : t -> bool
val is_bottom : t -> bool
@@ -95,12 +95,12 @@ module V : sig
val inject_float : Fval.t -> t
val interp_boolean : contains_zero:bool -> contains_non_zero:bool -> t
-(** [cast_int_to_int ~size ~signed v] applies to the abstract value [v] the
- conversion to the integer type described by [size] and [signed].
- Offsets of bases other than NULL are not clipped. If they were clipped,
- they should be clipped at the validity of the base. The C standard does
- not say that [p+(1ULL<<32+1)] is the same as [p+1], it says that
- [p+(1ULL<<32+1)] is invalid. *)
+ (** [cast_int_to_int ~size ~signed v] applies to the abstract value [v] the
+ conversion to the integer type described by [size] and [signed].
+ Offsets of bases other than NULL are not clipped. If they were clipped,
+ they should be clipped at the validity of the base. The C standard does
+ not say that [p+(1ULL<<32+1)] is the same as [p+1], it says that
+ [p+(1ULL<<32+1)] is invalid. *)
val cast_int_to_int: size:Int.t -> signed:bool -> t -> t
val reinterpret_as_float: Cil_types.fkind -> t -> t
@@ -174,9 +174,9 @@ module V_Or_Uninitialized : sig
include module type of Offsetmap_lattice_with_isotropy
with type t := t
- and type size_widen_hint = Location_Bytes.size_widen_hint
- and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
- and type widen_hint = Locations.Location_Bytes.widen_hint
+ and type size_widen_hint = Location_Bytes.size_widen_hint
+ and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
+ and type widen_hint = Locations.Location_Bytes.widen_hint
include Lattice_type.With_Under_Approximation with type t:= t
include Lattice_type.With_Narrow with type t := t
include Lattice_type.With_Top with type t := t
@@ -212,32 +212,32 @@ module V_Or_Uninitialized : sig
val reduce_by_initializedness : bool -> t -> t
(** [reduce_by_initializedness initialized v] reduces [v] so that its result
- [r] verifies [\initialized(r)] if [initialized] is [true], and
- [!\initialized(r)] otherwise. *)
+ [r] verifies [\initialized(r)] if [initialized] is [true], and
+ [!\initialized(r)] otherwise. *)
val reduce_by_danglingness : bool -> t -> t
(** [reduce_by_danglingness dangling v] reduces [v] so that its result [r]
- verifies [\dangling(r)] if [dangling] is [true], and
- [!\dangling(r)] otherwise. *)
+ verifies [\dangling(r)] if [dangling] is [true], and
+ [!\dangling(r)] otherwise. *)
val remove_indeterminateness: t -> t
(** Remove 'uninitialized' and 'escaping addresses' flags from the argument *)
- val unspecify_escaping_locals :
+ val unspecify_escaping_locals :
exact:bool -> (V.M.key -> bool) -> t -> bool * t
val map: (V.t -> V.t) -> t -> t
val map2: (V.t -> V.t -> V.t) -> t -> t -> t
(** initialized/escaping information is the join of the information
on each argument. *)
- end
+end
(** Memory slices. They are maps from intervals to values with
flags. All sizes and intervals are in bits. *)
module V_Offsetmap: sig
include module type of Offsetmap_sig
- with type v = V_Or_Uninitialized.t
- and type widen_hint = V_Or_Uninitialized.numerical_widen_hint
+ with type v = V_Or_Uninitialized.t
+ and type widen_hint = V_Or_Uninitialized.numerical_widen_hint
val narrow: t -> t -> t Bottom.Type.or_bottom
val narrow_reinterpret: t -> t -> t Bottom.Type.or_bottom
@@ -256,8 +256,8 @@ module Model: sig
(** Functions inherited from [Lmap_sig] interface *)
include module type of Lmap_sig
with type v = V_Or_Uninitialized.t
- and type offsetmap = V_Offsetmap.t
- and type widen_hint_base = V_Or_Uninitialized.numerical_widen_hint
+ and type offsetmap = V_Offsetmap.t
+ and type widen_hint_base = V_Or_Uninitialized.numerical_widen_hint
include Lattice_type.With_Narrow with type t := t
@@ -279,6 +279,7 @@ module Model: sig
- if [conflate_bottom] is [false] and at least one bit pointed to by
[l..l+loc.size-1] is not [V.bottom], the value is an approximation
of the join of all the bits at [l..l+loc.size-1].
+
As a rule of thumb, you must set [conflate_bottom=true] when the
operation you abstract really accesses [loc.size] bits, and when
undeterminate values are an error. This is typically the case when