Skip to content

GitLab

Commit fff2359b authored by Julien Signoles's avatar Julien Signoles
Browse files

make check-headers happy, bis

parent 2bf035d1
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/fixpoint.ml
View file @ fff2359b
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......@@ -210,4 +210,4 @@ let solve ieqs ivar chain_of_ivalmax =
let post_fixpoint =
iterate_till_post_fixpoint ieqs bottom chain_of_ivalmax
in
get_ival_of_iconst ivar post_fixpoint
\ No newline at end of file
get_ival_of_iconst ivar post_fixpoint
src/plugins/e-acsl/fixpoint.mli
View file @ fff2359b
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......@@ -75,4 +75,4 @@ val solve: Ieqs.t -> ival_exp -> Integer.t array -> Ival.t
val ivars_contains_ivar: ival_exp list -> ival_exp -> bool
(** [contains ivars ivar] checks whether the list of Ivar [ivars] contains the
Ivar [ivar]. *)
\ No newline at end of file
Ivar [ivar]. *)
src/plugins/e-acsl/lfunctions.ml
View file @ fff2359b
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......@@ -502,4 +502,4 @@ let lfunctions_visitor = object (self)
file)
end
let do_visit f = Visitor.visitFramacFile lfunctions_visitor f
\ No newline at end of file
let do_visit f = Visitor.visitFramacFile lfunctions_visitor f
src/plugins/e-acsl/lfunctions.mli
View file @ fff2359b
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......@@ -53,4 +53,4 @@ val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
val add_cast_ref:
(location -> Env.t -> typ option -> bool -> exp -> exp * Env.t) ref
\ No newline at end of file
(location -> Env.t -> typ option -> bool -> exp -> exp * Env.t) ref
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment