[eacsl] Move `runtime_check` from `Smart_stmt` to `Assert`

src/plugins/e-acsl/Makefile.in

@@ -74,11 +74,11 @@ CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))
 
 SRC_CODE_GENERATOR:= \
 	smart_exp \
-	assert \
 	smart_stmt \
 	gmp \
 	label \
 	env \
+	assert \
 	rational \
 	typed_number \
 	logic_functions \

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

@@ -90,3 +90,42 @@ let register_term ~loc kf env ?force t e adata =
 let register_pred ~loc kf env ?force p e adata =
   let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
   register ~loc kf env name ?force e adata
+
+let kind_to_string loc k =
+  Cil.mkString
+    ~loc
+    (match k with
+     | Smart_stmt.Assertion -> "Assertion"
+     | Smart_stmt.Precondition -> "Precondition"
+     | Smart_stmt.Postcondition -> "Postcondition"
+     | Smart_stmt.Invariant -> "Invariant"
+     | Smart_stmt.Variant -> "Variant"
+     | Smart_stmt.RTE -> "RTE")
+
+let runtime_check_with_msg ~loc msg ~pred_kind kind kf e =
+  let blocking =
+    match pred_kind with
+    | Assert -> Cil.one ~loc
+    | Check -> Cil.zero ~loc
+    | Admit ->
+      Options.fatal "No runtime check should be generated for 'admit' clauses"
+  in
+  let file = (fst loc).Filepath.pos_path in
+  let line = (fst loc).Filepath.pos_lnum in
+  Smart_stmt.rtl_call ~loc
+    "assert"
+    [ e;
+      blocking;
+      kind_to_string loc kind;
+      Cil.mkString ~loc (Functions.RTL.get_original_name kf);
+      Cil.mkString ~loc msg;
+      Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
+      Cil.integer loc line ]
+
+let runtime_check ~pred_kind kind kf e p =
+  let loc = p.pred_loc in
+  let msg =
+    Kernel.Unicode.without_unicode
+      (Format.asprintf "%a@?" Printer.pp_predicate) p
+  in
+  runtime_check_with_msg ~loc msg ~pred_kind kind kf e

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

@@ -92,3 +92,31 @@ val register_pred:
     corresponding to the predicate [p] to the assertion context [adata]. The
     parameter [force] has the same signification than for the function
     [register]. *)
+
+val runtime_check:
+  pred_kind:predicate_kind ->
+  Smart_stmt.annotation_kind ->
+  kernel_function ->
+  exp ->
+  predicate ->
+  stmt
+(** [runtime_check ~pred_kind kind kf e p] generates a runtime check for
+    predicate [p] by building a call to [__e_acsl_assert]. [e] (or [!e] if
+    [reverse] is set to [true]) is the C translation of [p], [kf] is the current
+    kernel_function, [kind] is the annotation kind of [p] and [pred_kind]
+    indicates if the assert should be blocking or not. *)
+
+val runtime_check_with_msg:
+  loc:location ->
+  string ->
+  pred_kind:predicate_kind ->
+  Smart_stmt.annotation_kind ->
+  kernel_function ->
+  exp ->
+  stmt
+(** [runtime_check_with_msg ~loc msg ~pred_kind kind kf e] generates a runtime
+    check for [e] (or [!e] if [reverse] is [true]) by building a call to
+    [__e_acsl_assert]. [msg] is the message printed if the runtime check fails.
+    [loc] is the location printed in the message if the runtime check fails.
+    [kf] is the current kernel_function, [kind] is the annotation kind of [p]
+    and [pred_kind] indicates if the assert should be blocking or not. *)

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

@@ -364,7 +364,7 @@ let check_requires kf kinstr env contract =
                      requires
                  in
                  let stmt =
-                   Smart_stmt.runtime_check
+                   Assert.runtime_check
                      ~pred_kind
                      Smart_stmt.Precondition
                      kf
@@ -498,7 +498,7 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env co
 
       (* Create assertions for complete and disjoint behaviors checks *)
       let create_assert_stmt bop msg =
-        Smart_stmt.runtime_check_with_msg
+        Assert.runtime_check_with_msg
           ~loc
           msg
           ~pred_kind:Assert
@@ -669,7 +669,7 @@ let check_post_conds kf kinstr env contract =
                          post_cond
                      in
                      let stmt =
-                       Smart_stmt.runtime_check
+                       Assert.runtime_check
                          ~pred_kind
                          Smart_stmt.Postcondition
                          kf

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

@@ -241,7 +241,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
       in
       let p = { p with pred_name = "array_coercion" :: p.pred_name } in
       let stmt =
-        Smart_stmt.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf e p
+        Assert.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf e p
       in
       stmt :: stmts, env
   in

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

@@ -108,7 +108,7 @@ let handle_annotations env kf stmt =
                 Printer.pp_term t
             in
             let stmt =
-              Smart_stmt.runtime_check_with_msg
+              Assert.runtime_check_with_msg
                 ~loc
                 msg
                 ~pred_kind:Assert
@@ -148,14 +148,14 @@ let handle_annotations env kf stmt =
             in
             let stmt =
               Smart_stmt.block_from_stmts [
-                Smart_stmt.runtime_check_with_msg
+                Assert.runtime_check_with_msg
                   ~loc
                   msg1
                   ~pred_kind:Assert
                   Smart_stmt.Variant
                   kf
                   variant_pos_e;
-                Smart_stmt.runtime_check_with_msg
+                Assert.runtime_check_with_msg
                   ~loc
                   msg2
                   ~pred_kind:Assert
@@ -300,7 +300,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
       | Some p ->
         let e, env = !predicate_to_exp_ref kf (Env.push env) p in
         let stmt, env =
-          Smart_stmt.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf e p, env
+          Assert.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf e p, env
         in
         let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
         let guard_for_small_type = Smart_stmt.block_stmt b in

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

@@ -39,25 +39,6 @@ let if_stmt ~loc ~cond ?(else_blk=Cil.mkBlock []) then_blk =
 
 let break ~loc = stmt (Break loc)
 
-type annotation_kind =
-  | Assertion
-  | Precondition
-  | Postcondition
-  | Invariant
-  | Variant
-  | RTE
-
-let kind_to_string loc k =
-  Cil.mkString
-    ~loc
-    (match k with
-     | Assertion -> "Assertion"
-     | Precondition -> "Precondition"
-     | Postcondition -> "Postcondition"
-     | Invariant -> "Invariant"
-     | Variant -> "Variant"
-     | RTE -> "RTE")
-
 let block stmt b = match b.bstmts with
   | [] ->
     (match stmt.skind with
@@ -179,33 +160,13 @@ let mark_readonly vi =
   let loc = vi.vdecl in
   rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
 
-let runtime_check_with_msg ~loc msg ~pred_kind kind kf e =
-  let blocking =
-    match pred_kind with
-    | Assert -> Cil.one ~loc
-    | Check -> Cil.zero ~loc
-    | Admit ->
-      Options.fatal "No runtime check should be generated for 'admit' clauses"
-  in
-  let file = (fst loc).Filepath.pos_path in
-  let line = (fst loc).Filepath.pos_lnum in
-  rtl_call ~loc
-    "assert"
-    [ e;
-      blocking;
-      kind_to_string loc kind;
-      Cil.mkString ~loc (Functions.RTL.get_original_name kf);
-      Cil.mkString ~loc msg;
-      Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
-      Cil.integer loc line ]
-
-let runtime_check ~pred_kind kind kf e p =
-  let loc = p.pred_loc in
-  let msg =
-    Kernel.Unicode.without_unicode
-      (Format.asprintf "%a@?" Printer.pp_predicate) p
-  in
-  runtime_check_with_msg ~loc msg ~pred_kind kind kf e
+type annotation_kind =
+  | Assertion
+  | Precondition
+  | Postcondition
+  | Invariant
+  | Variant
+  | RTE
 
 (*
 Local Variables:

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

@@ -107,25 +107,6 @@ type annotation_kind =
   | Variant
   | RTE
 
-val runtime_check:
-  pred_kind:predicate_kind -> annotation_kind -> kernel_function -> exp ->
-  predicate -> stmt
-(** [runtime_check ~pred_kind kind kf e p] generates a runtime check for
-    predicate [p] by building a call to [__e_acsl_assert]. [e] (or [!e] if
-    [reverse] is set to [true]) is the C translation of [p], [kf] is the current
-    kernel_function, [kind] is the annotation kind of [p] and [pred_kind]
-    indicates if the assert should be blocking or not. *)
-
-val runtime_check_with_msg:
-  loc:location -> string -> pred_kind:predicate_kind -> annotation_kind ->
-  kernel_function -> exp -> stmt
-(** [runtime_check_with_msg ~loc msg ~pred_kind kind kf e] generates a runtime
-    check for [e] (or [!e] if [reverse] is [true]) by building a call to
-    [__e_acsl_assert]. [msg] is the message printed if the runtime check fails.
-    [loc] is the location printed in the message if the runtime check fails.
-    [kf] is the current kernel_function, [kind] is the annotation kind of [p]
-    and [pred_kind] indicates if the assert should be blocking or not. *)
-
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

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

@@ -390,7 +390,7 @@ and context_insensitive_term_to_exp kf env t =
       let mk_stmts _v e =
         assert (Gmp_types.Z.is_t ty);
         let cond =
-          Smart_stmt.runtime_check
+          Assert.runtime_check
             ~pred_kind:Assert
             (Env.annotation_kind env)
             kf
@@ -475,7 +475,8 @@ and context_insensitive_term_to_exp kf env t =
           in
           let pname = bop_name ^ "_rhs_fits_in_mp_bitcnt_t" in
           let pred = { pred with pred_name = pname :: pred.pred_name } in
-          let cond = Smart_stmt.runtime_check
+          let cond =
+            Assert.runtime_check
               ~pred_kind:Assert
               Smart_stmt.RTE
               kf
@@ -540,7 +541,8 @@ and context_insensitive_term_to_exp kf env t =
           in
           let e1_guard_cond =
             let pred = Logic_const.prel ~loc (Rge, t1, zero) in
-            let cond = Smart_stmt.runtime_check
+            let cond =
+              Assert.runtime_check
                 ~pred_kind:Assert
                 Smart_stmt.RTE
                 kf
@@ -1138,7 +1140,7 @@ and translate_predicate ?pred_to_print kf env p =
     Env.add_stmt
       env
       kf
-      (Smart_stmt.runtime_check
+      (Assert.runtime_check
          ~pred_kind:p.tp_kind
          (Env.annotation_kind env)
          kf
@@ -1167,7 +1169,7 @@ let gmp_to_sizet ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
       Typing.type_named_predicate ~must_clear:false lower_guard;
       let lower_guard, env = predicate_to_exp kf env lower_guard in
       let assertion =
-        Smart_stmt.runtime_check
+        Assert.runtime_check
           ~pred_kind:Assert
           Smart_stmt.RTE
           kf
@@ -1192,7 +1194,7 @@ let gmp_to_sizet ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
   Typing.type_named_predicate ~must_clear:false upper_guard;
   let upper_guard, env = predicate_to_exp kf env upper_guard in
   let assertion =
-    Smart_stmt.runtime_check
+    Assert.runtime_check
       ~pred_kind:Assert
       Smart_stmt.RTE
       kf