[eacsl:codegen] Add a runtime check function that takes a string message

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

@@ -152,12 +152,7 @@ let mk_mark_readonly vi =
   let loc = vi.vdecl in
   mk_rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
 
-let mk_runtime_check ?(reverse=false) kind kf e p =
-  let loc = p.pred_loc in
-  let msg =
-    Kernel.Unicode.without_unicode
-      (Format.asprintf "%a@?" Printer.pp_predicate) p
-  in
+let mk_runtime_check_with_msg ?(reverse=false) ~loc msg kind kf e =
   let file = (fst loc).Filepath.pos_path in
   let line = (fst loc).Filepath.pos_lnum in
   let e =
@@ -174,6 +169,14 @@ let mk_runtime_check ?(reverse=false) kind kf e p =
       Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
       Cil.integer loc line ]
 
+let mk_runtime_check ?(reverse=false) kind kf e p =
+  let loc = p.pred_loc in
+  let msg =
+    Kernel.Unicode.without_unicode
+      (Format.asprintf "%a@?" Printer.pp_predicate) p
+  in
+  mk_runtime_check_with_msg ~reverse ~loc msg kind kf e
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

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

@@ -85,6 +85,15 @@ val mk_runtime_check:
     [true]) is the C translation of [p], [kf] is the current kernel_function and
     [kind] is the annotation kind of [p]. *)
 
+val mk_runtime_check_with_msg:
+  ?reverse:bool -> loc:location -> string -> annotation_kind ->
+  kernel_function -> exp -> stmt
+(** [mk_runtime_check_with_msg kind kf e msg] 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 and [kind] is the annotation kind of [p]. *)
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."