[e-acsl] add support for Here label in functions and predicates

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

@@ -77,12 +77,13 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
   match p.pred_content with
   | Pfalse -> Cil.zero ~loc, adata, env
   | Ptrue -> Cil.one ~loc, adata, env
-  | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
-  | Papp (li, [], args) ->
+  | Papp (li, [], args)
+  | Papp (li, [BuiltinLabel Here], args) ->
     let e, adata, env =
       Logic_functions.app_to_exp ~adata ~loc kf env li args in
     let adata = Assert.register_pred ~loc env p e adata in
     e, adata, env
+  | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
   | Pdangling _ -> Env.not_yet env "\\dangling"
   | Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
   | Pvalid_function _ -> Env.not_yet env "\\valid_function"

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

@@ -765,7 +765,8 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
   | Tapp(li, _, _)
     when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
     assert false
-  | Tapp(li, [], args) ->
+  | Tapp(li, [], args)
+  | Tapp(li, [BuiltinLabel Here], args) ->
     let e, adata, env =
       Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args in
     let adata = Assert.register_term ~loc t e adata in

src/plugins/e-acsl/tests/arith/functions.c

@@ -37,8 +37,8 @@ int glob = 5;
 /*@ logic double f2(double x) = (double)(1/x); */ /* handle in MR !226 */
 
 // To test not_yet:
-/*@ predicate p_notyet{L}(integer x) = x > 0; */
-/*@ logic integer f_notyet{L}(integer x) = x; */
+/*@ predicate p_here{L}(integer x) = x > 0; */
+/*@ logic integer f_here{L}(integer x) = x; */
 
 // Test sums inside functions
 /*@ logic integer f_sum (integer x) = \sum(1,x,\lambda integer y; 1); */
@@ -83,6 +83,6 @@ int main(void) {
   /*@ assert over(1., 2.) == 0.5; */;
 
   // not yet supported
-  /* /\*@ assert p_notyet(27); *\/ ; */
-  /* /\*@ assert f_notyet(27) == 27; *\/ ; */
+  /*@ assert p_here(27); */;
+  /*@ assert f_here(27) == 27; */;
 }

src/plugins/e-acsl/tests/arith/oracle/gen_functions.c

@@ -83,10 +83,14 @@ int glob = 5;
  */
 double __gen_e_acsl_f2(double x);
 
-/*@ predicate p_notyet{L}(integer x) = x > 0;
+/*@ predicate p_here{L}(integer x) = x > 0;
  */
-/*@ logic integer f_notyet{L}(integer x) = x;
+int __gen_e_acsl_p_here(int x);
+
+/*@ logic integer f_here{L}(integer x) = x;
  */
+int __gen_e_acsl_f_here(int x);
+
 /*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1);
  */
 int __gen_e_acsl_f_sum(int x);
@@ -434,6 +438,41 @@ int main(void)
     __gmpq_clear(__gen_e_acsl__11);
   }
   /*@ assert over(1., 2.) == 0.5; */ ;
+  {
+    int __gen_e_acsl_p_here_2;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data_16 =
+      {.values = (void *)0};
+    __gen_e_acsl_p_here_2 = __gen_e_acsl_p_here(27);
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,"p_here(27)",
+                                 0,__gen_e_acsl_p_here_2);
+    __gen_e_acsl_assert_data_16.blocking = 1;
+    __gen_e_acsl_assert_data_16.kind = "Assertion";
+    __gen_e_acsl_assert_data_16.pred_txt = "p_here(27)";
+    __gen_e_acsl_assert_data_16.file = "functions.c";
+    __gen_e_acsl_assert_data_16.fct = "main";
+    __gen_e_acsl_assert_data_16.line = 86;
+    __e_acsl_assert(__gen_e_acsl_p_here_2,& __gen_e_acsl_assert_data_16);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data_16);
+  }
+  /*@ assert p_here(27); */ ;
+  {
+    int __gen_e_acsl_f_here_2;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data_17 =
+      {.values = (void *)0};
+    __gen_e_acsl_f_here_2 = __gen_e_acsl_f_here(27);
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_17,"f_here(27)",
+                                 0,__gen_e_acsl_f_here_2);
+    __gen_e_acsl_assert_data_17.blocking = 1;
+    __gen_e_acsl_assert_data_17.kind = "Assertion";
+    __gen_e_acsl_assert_data_17.pred_txt = "f_here(27) == 27";
+    __gen_e_acsl_assert_data_17.file = "functions.c";
+    __gen_e_acsl_assert_data_17.fct = "main";
+    __gen_e_acsl_assert_data_17.line = 87;
+    __e_acsl_assert(__gen_e_acsl_f_here_2 == 27,
+                    & __gen_e_acsl_assert_data_17);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data_17);
+  }
+  /*@ assert f_here(27) == 27; */ ;
   __retres = 0;
   __e_acsl_memory_clean();
   return __retres;
@@ -638,6 +677,21 @@ double __gen_e_acsl_f2(double x)
   return __gen_e_acsl__9;
 }
 
+/*@ assigns \result;
+    assigns \result \from x; */
+int __gen_e_acsl_p_here(int x)
+{
+  int __retres = x > 0;
+  return __retres;
+}
+
+/*@ assigns \result;
+    assigns \result \from x; */
+int __gen_e_acsl_f_here(int x)
+{
+  return x;
+}
+
 /*@ assigns \result;
     assigns \result \from x; */
 int __gen_e_acsl_f_sum(int x)