diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index b889109f461ee67f67d95f3b46a0b4aab004edd1..6b7856f0e2b1f819875b2c3d337bb855d9e38540 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -32,11 +32,11 @@ end
module Translate: sig
exception No_simple_translation of term
val term_to_exp: typ option -> term -> exp
-(** @raise New_typing_error when the given term cannot be typed (something wrong
- happened with this term)
- @raise Not_yet when the given term contains an unsupported construct.
- @raise No_simple_translation when the given term cannot be translated into
- a single expression. *)
+ (** @raise New_typing_error when the given term cannot be typed (something wrong
+ happened with this term)
+ @raise Not_yet when the given term contains an unsupported construct.
+ @raise No_simple_translation when the given term cannot be translated into
+ a single expression. *)
end
(** No function is directly exported: they are dynamically registered. *)
diff --git a/src/plugins/e-acsl/demo/script.ml b/src/plugins/e-acsl/demo/script.ml
index 03036b425d0497ce4ade6558cb4c74aa9b0f2ba7..5c61595d99b3af283f52eeb3bdbad942a2f28334 100644
--- a/src/plugins/e-acsl/demo/script.ml
+++ b/src/plugins/e-acsl/demo/script.ml
@@ -5,38 +5,38 @@ open Cil_types
(* ************************************************************************** *)
include Plugin.Register(struct
- let name = "txt2ppt"
- let shortname = "t2p"
- let help = "Convert E-ACSL textual properties to Frama-C properties"
-end)
+ let name = "txt2ppt"
+ let shortname = "t2p"
+ let help = "Convert E-ACSL textual properties to Frama-C properties"
+ end)
(* ************************************************************************** *)
(* Defining plug-in's options *)
(* ************************************************************************** *)
-module Fct_name =
+module Fct_name =
Empty_string
(struct
- let option_name = "-ppt-fct"
+ let option_name = "-ppt-fct"
let help = "Name of the function in which the property is defined"
let arg_name = ""
- end)
+ end)
-module Ppt_name =
+module Ppt_name =
Empty_string
(struct
- let option_name = "-ppt-name"
+ let option_name = "-ppt-name"
let help = "Name of the property (assertion, ...)"
let arg_name = ""
- end)
+ end)
-module Ppt_line =
+module Ppt_line =
Zero
(struct
- let option_name = "-ppt-line"
+ let option_name = "-ppt-line"
let help = "Line at which the property is defined"
let arg_name = ""
- end)
+ end)
(* ************************************************************************** *)
(* Searching the property according to plug-in's options *)
@@ -48,19 +48,19 @@ let search_assert_or_invariant kf =
try
Annotations.iter_all_code_annot
(fun stmt _ a ->
- match a.annot_content with
- | AAssert(_, _, p) | AInvariant(_, _, p) ->
- let line = Ppt_line.get () in
- if (fst (p.loc)).Lexing.pos_lnum = line then
- raise (Found(Property.ip_of_code_annot_single kf stmt a, line))
- | _ -> ());
+ match a.annot_content with
+ | AAssert(_, _, p) | AInvariant(_, _, p) ->
+ let line = Ppt_line.get () in
+ if (fst (p.loc)).Lexing.pos_lnum = line then
+ raise (Found(Property.ip_of_code_annot_single kf stmt a, line))
+ | _ -> ());
assert false
with Found(ppt, line) ->
ppt, line
let is_predicate p line = (fst (p.ip_loc)).Lexing.pos_lnum = line
-let search_funspec_part iter convert kf =
+let search_funspec_part iter convert kf =
try
Annotations.iter_behaviors
(fun _ bhv -> iter (fun _ a -> convert bhv a) kf bhv.b_name)
@@ -69,22 +69,22 @@ let search_funspec_part iter convert kf =
with Found(ppt, line) ->
ppt, line
-let search_ensures kf =
- search_funspec_part
+let search_ensures kf =
+ search_funspec_part
Annotations.iter_ensures
(fun bhv (_, p as a) ->
- let line = Ppt_line.get () in
- if is_predicate p line then
- raise (Found (Property.ip_of_ensures kf Kglobal bhv a, line)) )
+ let line = Ppt_line.get () in
+ if is_predicate p line then
+ raise (Found (Property.ip_of_ensures kf Kglobal bhv a, line)) )
kf
-let search_requires kf =
+let search_requires kf =
search_funspec_part
Annotations.iter_requires
(fun bhv a ->
- let line = Ppt_line.get () in
- if is_predicate a line then
- raise (Found (Property.ip_of_requires kf Kglobal bhv a, line)) )
+ let line = Ppt_line.get () in
+ if is_predicate a line then
+ raise (Found (Property.ip_of_requires kf Kglobal bhv a, line)) )
kf
let search kf = match Ppt_name.get () with
@@ -97,7 +97,7 @@ let search kf = match Ppt_name.get () with
(* Emitting status "invalid" for the property *)
(* ************************************************************************** *)
-let emitter =
+let emitter =
Emitter.create "E-ACSL" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
let emit ppt line =
@@ -108,7 +108,7 @@ let emit ppt line =
(* Plug-in's main *)
(* ************************************************************************** *)
-let main () =
+let main () =
let kf = Globals.Functions.find_by_name (Fct_name.get ()) in
let ppt, line = search kf in
emit ppt line
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 602461c6e5816c00cf7d23bbcb5f019f6874b34f..18e2b851269addf0d63ca754e7fb1de743e19fe8 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -33,24 +33,24 @@ let align_error s = raise (Alignment_error s)
* - [attrs] has a single align attribute with a value which is less than [algn] *)
let sufficiently_aligned attrs algn =
let alignment = List.fold_left (fun acc attr ->
- match attr with
- | Attr("align", [AInt i]) ->
- let alignment = Integer.to_int i in
- if acc <> 0 && acc <> alignment then
- (* Multiple align attributes with different values *)
- align_error "Multiple alignment attributes"
- else if alignment < algn then
- (* If there is an alignment attribute it should be greater
- * or equal to [algn] *)
- align_error "Insufficient alignment"
- else
- alignment
- | Attr("align", _) ->
- (* Align attribute with an argument other than a single number,
- should not happen really *)
- assert false
- | _ -> acc
- ) 0 attrs in alignment > 0
+ match attr with
+ | Attr("align", [AInt i]) ->
+ let alignment = Integer.to_int i in
+ if acc <> 0 && acc <> alignment then
+ (* Multiple align attributes with different values *)
+ align_error "Multiple alignment attributes"
+ else if alignment < algn then
+ (* If there is an alignment attribute it should be greater
+ * or equal to [algn] *)
+ align_error "Insufficient alignment"
+ else
+ alignment
+ | Attr("align", _) ->
+ (* Align attribute with an argument other than a single number,
+ should not happen really *)
+ assert false
+ | _ -> acc
+ ) 0 attrs in alignment > 0
(* Given the type and the list of attributes of [varinfo] ([fieldinfo]) return
* true if that [varinfo] ([fieldinfo]) requires to be aligned at the boundary
@@ -65,14 +65,14 @@ class prepare_visitor prj = object (self)
method !vblock _ =
if Options.Temporal_validity.get () then
Cil.DoChildrenPost (fun blk ->
- List.iter (fun vi ->
- (* 4 bytes alignment is required to allow sufficient space for storage
- of 32-bit timestamps in a 1:1 shadow. *)
- if require_alignment vi.vtype vi.vattr 4; then begin
- vi.vattr <- Attr("aligned",[AInt Integer.four]) :: vi.vattr
- end)
- blk.blocals;
- blk)
+ List.iter (fun vi ->
+ (* 4 bytes alignment is required to allow sufficient space for storage
+ of 32-bit timestamps in a 1:1 shadow. *)
+ if require_alignment vi.vtype vi.vattr 4; then begin
+ vi.vattr <- Attr("aligned",[AInt Integer.four]) :: vi.vattr
+ end)
+ blk.blocals;
+ blk)
else
Cil.DoChildren
@@ -92,17 +92,17 @@ class prepare_visitor prj = object (self)
s.spec_terminates;
List.iter
(fun l ->
- push kf K_Complete (Property.ip_of_complete kf kinstr ~active:[] l))
+ push kf K_Complete (Property.ip_of_complete kf kinstr ~active:[] l))
s.spec_complete_behaviors;
List.iter
(fun l ->
- push kf K_Disjoint (Property.ip_of_disjoint kf kinstr ~active:[] l))
+ push kf K_Disjoint (Property.ip_of_disjoint kf kinstr ~active:[] l))
s.spec_disjoint_behaviors;
List.iter
(fun b ->
- List.iter
- (fun p -> push kf K_Requires (Property.ip_of_requires kf kinstr b p))
- b.b_requires)
+ List.iter
+ (fun p -> push kf K_Requires (Property.ip_of_requires kf kinstr b p))
+ b.b_requires)
s.spec_behavior
method private push_post_spec spec =
@@ -160,14 +160,14 @@ class prepare_visitor prj = object (self)
| AExtended _ -> () (* never translate extensions *)
method private push_post_code_annot a = match a.annot_content with
- | AStmtSpec(_ (* TODO *), s) -> self#push_post_spec s
- | AAssert _
- | AInvariant _
- | AVariant _
- | AAssigns _
- | AAllocation _
- | APragma _
- | AExtended _ -> ()
+ | AStmtSpec(_ (* TODO *), s) -> self#push_post_spec s
+ | AAssert _
+ | AInvariant _
+ | AVariant _
+ | AAssigns _
+ | AAllocation _
+ | APragma _
+ | AExtended _ -> ()
(* Move variable declared in the body of a switch statement to the outer
scope *)
@@ -177,17 +177,17 @@ class prepare_visitor prj = object (self)
init_stmt;
Cil.DoChildrenPost
(fun stmt ->
- Annotations.iter_code_annot
- (fun _ a -> self#push_post_code_annot a)
- init_stmt;
- match stmt.skind with
- | Switch(_,sw_blk,_,_) ->
- let new_blk = Cil.mkBlock [ stmt ] in
- let new_stmt = Cil.mkStmt (Block new_blk) in
- new_blk.blocals <- sw_blk.blocals;
- sw_blk.blocals <- [];
- new_stmt
- | _ -> stmt)
+ Annotations.iter_code_annot
+ (fun _ a -> self#push_post_code_annot a)
+ init_stmt;
+ match stmt.skind with
+ | Switch(_,sw_blk,_,_) ->
+ let new_blk = Cil.mkBlock [ stmt ] in
+ let new_stmt = Cil.mkStmt (Block new_blk) in
+ new_blk.blocals <- sw_blk.blocals;
+ sw_blk.blocals <- [];
+ new_stmt
+ | _ -> stmt)
method private is_unvariadic_function vi =
match Cil.unrollType vi.vtype with
@@ -195,24 +195,24 @@ class prepare_visitor prj = object (self)
| _ -> false
method !vglob_aux = function
- | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
+ | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
when self#is_unvariadic_function vi
&& not (Misc.is_library_loc loc)
&& not (Cil.is_builtin vi)
- ->
- let kf = Extlib.the self#current_kf in
- let s = Annotations.funspec ~populate:false kf in
- Cil.DoChildrenPost
- (fun f ->
- self#push_pre_spec s;
- self#push_post_spec s;
- f)
- | _ ->
- Cil.DoChildren
+ ->
+ let kf = Extlib.the self#current_kf in
+ let s = Annotations.funspec ~populate:false kf in
+ Cil.DoChildrenPost
+ (fun f ->
+ self#push_pre_spec s;
+ self#push_post_spec s;
+ f)
+ | _ ->
+ Cil.DoChildren
initializer Project.copy ~selection:(Parameter_state.get_selection ()) prj
- end
+end
let prepare () =
Options.feedback ~level:2 "prepare AST for E-ACSL transformations";