lint

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. *)

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

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";