[eacsl] Fix lines > 80 characters

src/plugins/e-acsl/E_ACSL.mli

@@ -52,8 +52,9 @@ end
 module Functions: sig
   module RTL: sig
     val is_generated_name: string -> bool
-    (** @return [true] if the prefix of the given name indicates that it has been
-        generated by E-ACSL instrumentation (see [mk_gen_name] function). *)
+    (** @return [true] if the prefix of the given name indicates that it has
+        been generated by E-ACSL instrumentation (see [mk_gen_name] function).
+    *)
   end
 end
 

src/plugins/e-acsl/src/code_generator/contract.ml

@@ -448,13 +448,15 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env co
     let must_translate_complete =
       match ppt_to_translate with
       | Both | Complete ->
-        Translate_utils.must_translate (Property.ip_of_complete kf kinstr ~active bhvrs_list)
+        Translate_utils.must_translate
+          (Property.ip_of_complete kf kinstr ~active bhvrs_list)
       | Disjoint -> false
     in
     let must_translate_disjoint =
       match ppt_to_translate with
       | Both | Disjoint ->
-        Translate_utils.must_translate (Property.ip_of_disjoint kf kinstr ~active bhvrs_list)
+        Translate_utils.must_translate
+          (Property.ip_of_disjoint kf kinstr ~active bhvrs_list)
       | Complete -> false
     in
 
@@ -570,8 +572,8 @@ let check_complete_and_disjoint kf kinstr env contract =
        - The disjoint list
 
        The behaviors of a clause are stored in a Set so that they are
-       automatically sorted, the duplicates are removed, and they can be compared
-       for equality.
+       automatically sorted, the duplicates are removed, and they can be
+       compared for equality.
     *)
     let completes =
       List.map
@@ -599,7 +601,9 @@ let check_complete_and_disjoint kf kinstr env contract =
     in
     (* Create a common variable to hold the number of active behavior for the
        current check *)
-    let get_or_create_var = mk_get_or_create_var kf Cil.intType "active_bhvrs" in
+    let get_or_create_var =
+      mk_get_or_create_var kf Cil.intType "active_bhvrs"
+    in
     (* Check the complete and disjoint clauses *)
     let check_bhvrs env ppt_to_translate bhvrs =
       check_active_behaviors

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -648,8 +648,8 @@ let inject_in_global (env, main) global =
     ~fun_def
     global
 
-(* Insert [stmt_begin] as the first statement of [fundec] and insert [stmt_end] as
-   the last before [return] *)
+(* Insert [stmt_begin] as the first statement of [fundec] and insert [stmt_end]
+   as the last before [return] *)
 let surround_function_with kf fundec stmt_begin stmt_end =
   let body = fundec.sbody in
   (* Insert last statement *)

src/plugins/e-acsl/src/code_generator/translate_annots.ml

@@ -34,13 +34,15 @@ let pre_funspec kf kinstr env funspec =
     unsupported
       (fun spec ->
          let ppt = Property.ip_decreases_of_spec kf kinstr spec in
-         if Translate_utils.must_translate_opt ppt then Env.not_yet env "decreases clause")
+         if Translate_utils.must_translate_opt ppt
+         then Env.not_yet env "decreases clause")
       funspec;
     (* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
     unsupported
       (fun spec ->
          let ppt = Property.ip_terminates_of_spec kf kinstr spec in
-         if Translate_utils.must_translate_opt ppt then Env.not_yet env "terminates clause")
+         if Translate_utils.must_translate_opt ppt
+         then Env.not_yet env "terminates clause")
       funspec;
     env
   in
@@ -58,7 +60,8 @@ let post_funspec kf kinstr env =
 let pre_code_annotation kf stmt env annot =
   let convert env = match annot.annot_content with
     | AAssert(l, p) ->
-      if Translate_utils.must_translate (Property.ip_of_code_annot_single kf stmt annot) then
+      if Translate_utils.must_translate
+          (Property.ip_of_code_annot_single kf stmt annot) then
         let env = Env.set_annotation_kind env Smart_stmt.Assertion in
         if l <> [] then
           Env.not_yet env "@[assertion applied only on some behaviors@]";
@@ -75,7 +78,8 @@ let pre_code_annotation kf stmt env annot =
         ~f:(fun env ->
             Contract.translate_preconditions kf (Kstmt stmt) env contract)
     | AInvariant(l, loop_invariant, p) ->
-      if Translate_utils.must_translate (Property.ip_of_code_annot_single kf stmt annot) then
+      if Translate_utils.must_translate
+          (Property.ip_of_code_annot_single kf stmt annot) then
         let env = Env.set_annotation_kind env Smart_stmt.Invariant in
         if l <> [] then
           Env.not_yet env "@[invariant applied only on some behaviors@]";
@@ -89,7 +93,8 @@ let pre_code_annotation kf stmt env annot =
       else
         env
     | AVariant (t, measure) ->
-      if Translate_utils.must_translate (Property.ip_of_code_annot_single kf stmt annot)
+      if Translate_utils.must_translate
+          (Property.ip_of_code_annot_single kf stmt annot)
       then Env.set_loop_variant env ?measure t
       else env
     | AAssigns _ ->
@@ -97,13 +102,17 @@ let pre_code_annotation kf stmt env annot =
          to be fixed when implementing e-acsl#29 *)
       let ppts = Property.ip_of_code_annot kf stmt annot in
       List.iter
-        (fun ppt -> if Translate_utils.must_translate ppt then Env.not_yet env "assigns")
+        (fun ppt ->
+           if Translate_utils.must_translate ppt
+           then Env.not_yet env "assigns")
         ppts;
       env
     | AAllocation _ ->
       let ppts = Property.ip_of_code_annot kf stmt annot in
       List.iter
-        (fun ppt -> if Translate_utils.must_translate ppt then Env.not_yet env "allocation")
+        (fun ppt ->
+           if Translate_utils.must_translate ppt
+           then Env.not_yet env "allocation")
         ppts;
       env
     | APragma _ -> Env.not_yet env "pragma"

src/plugins/e-acsl/src/code_generator/translate_predicates.ml

@@ -86,7 +86,16 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
     let ity =
       Typing.get_integer_op_of_predicate ~lenv p
     in
-    Translate_utils.comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
+    Translate_utils.comparison_to_exp
+      ~adata
+      ~loc
+      kf
+      env
+      ity
+      (relation_to_binop rel)
+      t1
+      t2
+      None
   | Pand(p1, p2) ->
     (* p1 && p2 <==> if p1 then p2 else false *)
     Extlib.flatten
@@ -193,7 +202,9 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
     else begin
       (* convert [t'] to [e] in a separated local env *)
       let e, adata, env = to_exp ~adata kf (Env.push env) p' in
-      let e, env, sty = Translate_utils.at_to_exp_no_lscope kf env None label e in
+      let e, env, sty =
+        Translate_utils.at_to_exp_no_lscope kf env None label e
+      in
       assert (sty = Typed_number.C_number);
       let adata, env = Assert.register_pred ~loc kf env p e adata in
       e, adata, env
@@ -227,7 +238,12 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
            let tp = Logic_const.toplevel_predicate ~kind:Assert p in
            let annot = Logic_const.new_code_annotation (AAssert ([],tp)) in
            Typing.preprocess_rte (Env.Local_vars.get env) annot;
-           !translate_rte_annots_ref Printer.pp_code_annotation annot kf env [annot]
+           !translate_rte_annots_ref
+             Printer.pp_code_annotation
+             annot
+             kf
+             env
+             [annot]
         )
         env
         tlist

src/plugins/e-acsl/src/code_generator/translate_rtes.mli

@@ -34,7 +34,12 @@ val rte_annots:
 (** Translate the given RTE annotations into runtime checks in the given
     environment. *)
 
-val exp: ?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp -> Env.t
+val exp:
+  ?filter:(code_annotation -> bool) ->
+  kernel_function ->
+  Env.t ->
+  exp ->
+  Env.t
 (** Generate RTE annotations from the given expression and translate them in the
     given environment. *)
 

src/plugins/e-acsl/src/code_generator/translate_terms.ml

@@ -86,8 +86,9 @@ let constant_to_exp ~loc env t c =
     else mk_real lr.r_literal
   | LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), Typed_number.C_number
 
-(* Create and initialize a variable in the [env] according to [ty], [name] and [exp_init],
-   return a tuple [varinfo * exp] and the [env] extended with the new variable. *)
+(* Create and initialize a variable in the [env] according to [ty], [name] and
+   [exp_init], return a tuple [varinfo * exp] and the [env] extended with the
+   new variable. *)
 let create_and_init_var ~loc kf ty name exp_init env =
   Env.new_var
     ~loc
@@ -371,9 +372,10 @@ and context_insensitive_term_to_exp ~adata kf env t =
     let e1, adata, env = to_exp ~adata kf env t1 in
     let t2_to_exp adata env = to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
-      (* Creating a second assertion context that will hold the data contributing
-         to the guard of the denominator. The context will be merged to [adata]
-         afterward so that the calling assertion context holds all data. *)
+      (* Creating a second assertion context that will hold the data
+         contributing to the guard of the denominator. The context will be
+         merged to [adata] afterward so that the calling assertion context holds
+         all data. *)
       let adata2, env = Assert.empty ~loc kf env in
       let e2, adata2, env = t2_to_exp adata2 env in
       let adata, env = Assert.merge_right ~loc kf env adata2 adata in
@@ -391,7 +393,17 @@ and context_insensitive_term_to_exp ~adata kf env t =
       let guard, _, env =
         let name = Misc.name_of_binop bop ^ "_guard" in
         Translate_utils.comparison_to_exp
-          ~adata:Assert.no_data ~loc kf env Typing.gmpz ~e1:e2 ~name Ne t2 zero t
+          ~adata:Assert.no_data
+          ~loc
+          kf
+          env
+          Typing.gmpz
+          ~e1:e2
+          ~name
+          Ne
+          t2
+          zero
+          t
       in
       let p = Logic_const.prel ~loc (Rneq, t2, zero) in
       let cond, env =
@@ -428,7 +440,16 @@ and context_insensitive_term_to_exp ~adata kf env t =
     (* comparison operators *)
     let ity = Typing.get_integer_op ~lenv t in
     let e, adata, env =
-      Translate_utils.comparison_to_exp ~adata ~loc kf env ity bop t1 t2 (Some t)
+      Translate_utils.comparison_to_exp
+        ~adata
+        ~loc
+        kf
+        env
+        ity
+        bop
+        t1
+        t2
+        (Some t)
     in
     e, adata, env, Typed_number.C_number, ""
   | TBinOp((Shiftlt | Shiftrt) as bop, t1, t2) ->
@@ -761,7 +782,13 @@ and context_insensitive_term_to_exp ~adata kf env t =
                let res3 = e3, env3 in
                Extlib.nest
                  adata
-                 (Translate_utils.conditional_to_exp ~loc kf (Some t) e1 res2 res3)
+                 (Translate_utils.conditional_to_exp
+                    ~loc
+                    kf
+                    (Some t)
+                    e1
+                    res2
+                    res3)
              ))
     in
     e, adata, env, Typed_number.C_number, ""
@@ -777,7 +804,9 @@ and context_insensitive_term_to_exp ~adata kf env t =
       e, adata, env, Typed_number.C_number, ""
     else
       let e, _, env = to_exp ~adata:Assert.no_data kf (Env.push env) t' in
-      let e, env, sty = Translate_utils.at_to_exp_no_lscope kf env (Some t) label e in
+      let e, env, sty =
+        Translate_utils.at_to_exp_no_lscope kf env (Some t) label e
+      in
       let adata, env = Assert.register_term ~loc kf env t e adata in
       e, adata, env, sty, ""
   | Tbase_addr(BuiltinLabel Here, t') ->
@@ -848,7 +877,9 @@ and to_exp ~adata kf env t =
            let e, adata, env, sty, name =
              context_insensitive_term_to_exp ~adata kf env t
            in
-           let env = if generate_rte then !translate_rte_exp_ref kf env e else env in
+           let env =
+             if generate_rte then !translate_rte_exp_ref kf env e else env
+           in
            let cast = Typing.get_cast ~lenv:(Env.Local_vars.get env) t in
            let name = if name = "" then None else Some name in
            Extlib.nest