[typing] fix one incorrect assertion

src/plugins/e-acsl/new_typing.ml

@@ -219,7 +219,7 @@ let rec type_term env ~ctx t =
       ignore (type_term env ~ctx t2);
       ctx
     | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
-      assert (compare ctx c_int >= 1);
+      assert (compare ctx c_int >= 0);
       let ctx =
         try
           let i1 = Interval.infer env t1 in
@@ -302,7 +302,7 @@ let rec type_term env ~ctx t =
       Other
 
     | TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
-(*      Options.feedback "BIN PI"; (* HERE *)*)
+(*      Options.feedback "BIN PI %a ; %a" Printer.pp_term t1 Printer.pp_term t2; (* HERE *)*)
       (* it is a pointer, as well as [t1], while [t2] is a size_t.
          Both [t1] and [t2] must be typed. *)
       ignore (type_term env ~ctx:Other t1);
@@ -438,12 +438,12 @@ let rec type_predicate_named env p =
   coerce ~ctx:c_int ty
 
 let type_term ~ctx t =
-  Options.feedback ~dkey ~level:4 "typing term %a."
-    Printer.pp_term t;
+  Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
+    Printer.pp_term t pretty ctx;
   ignore (type_term Interval.Env.empty ~ctx t)
 
 let type_named_predicate ?(must_clear=true) p =
-  Options.feedback ~dkey ~level:3 "typing predicate %a."
+  Options.feedback ~dkey ~level:3 "typing predicate '%a'."
     Printer.pp_predicate_named p;
   if must_clear then Memo.clear ();
   ignore (type_predicate_named Interval.Env.empty p)

src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c

@@ -80,20 +80,20 @@ int __gen_e_acsl_sorted(int *t, int n)
       {
         int __gen_e_acsl_valid_read;
         int __gen_e_acsl_valid_read_2;
-        __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_i),
+        __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + (unsigned long)((unsigned int)__gen_e_acsl_i)),
                                                       sizeof(int));
         __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
                         (char *)"sorted",
-                        (char *)"mem_access: \\valid_read(t+__gen_e_acsl_i)",
+                        (char *)"mem_access: \\valid_read(t+(unsigned long)__gen_e_acsl_i)",
                         6);
-        __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (
-                                                                 (long)__gen_e_acsl_i - (long)1)),
+        __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (unsigned long)(
+                                                                 __gen_e_acsl_i - 1)),
                                                         sizeof(int));
         __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
                         (char *)"sorted",
-                        (char *)"mem_access: \\valid_read(t+(long)((long)__gen_e_acsl_i-1))",
+                        (char *)"mem_access: \\valid_read(t+(unsigned long)((long)(__gen_e_acsl_i-1)))",
                         6);
-        if (*(t + ((long)__gen_e_acsl_i - (long)1)) <= *(t + __gen_e_acsl_i)) 
+        if (*(t + (unsigned long)(__gen_e_acsl_i - 1)) <= *(t + (unsigned long)__gen_e_acsl_i)) 
           ;
         else {
           __gen_e_acsl_forall = 0;

src/plugins/e-acsl/translate.ml

@@ -550,7 +550,8 @@ and mmodel_call_with_size ~loc kf name ctx env t =
           | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
           | _ -> assert false
         in
-        [ Misc.mk_call ~loc ~result:(Cil.var v) ("__" ^ name) [ e; sizeof ] ])
+        [ Misc.mk_call
+            ~loc ~result:(Cil.var v) (Misc.mk_api_name name) [ e; sizeof ] ])
   in
   res, env