[E-ACSL] export a simple version of predicate_to_exp

src/plugins/e-acsl/main.ml

@@ -70,6 +70,15 @@ let generate_code =
     (Datatype.func Datatype.string Project.ty)
     generate_code
 
+let predicate_to_exp =
+  Dynamic.register
+    ~plugin:"e-acsl"
+    ~journalize:false
+    "predicate_to_exp"
+    (Datatype.func2
+       Kernel_function.ty Cil_datatype.Predicate_named.ty Cil_datatype.Exp.ty)
+    Translate.predicate_to_exp
+
 let add_e_acsl_library () =
   if Options.must_visit () then begin
     Kernel.CppExtraArgs.add (Pretty_utils.sfprintf " -I%s/libc" Config.datadir);

src/plugins/e-acsl/translate.ml

@@ -606,6 +606,13 @@ let () =
   Quantif.term_to_exp_ref := term_to_exp;
   Quantif.named_predicate_to_exp_ref := named_predicate_to_exp
 
+let predicate_to_exp kf p =
+  Typing.type_named_predicate ~must_clear:true p;
+  let empty_env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
+  let e, _ = named_predicate_to_exp kf empty_env p in
+  assert (Typ.equal (Cil.typeOf e) Cil.intType);
+  e  
+
 (* ************************************************************************** *)
 (* [translate_*] translates a given ACSL annotation into the corresponding C
    statement (if any) for runtime assertion checking *)

src/plugins/e-acsl/translate.mli

@@ -33,6 +33,8 @@ val translate_pre_code_annotation:
 val translate_post_code_annotation: 
   kernel_function -> Env.t -> code_annotation -> Env.t
 
+val predicate_to_exp: kernel_function -> predicate named -> exp
+
 (*
 Local Variables:
 compile-command: "make"