[aorai] register Frama_C_aorai_show_state as builtin

src/plugins/aorai/aorai_eva_analysis.enabled.ml

@@ -34,10 +34,19 @@ let show_aorai_variable state fmt var_name =
        Z.Overflow | Not_found ->
     Format.fprintf fmt "?"
 
-let builtin_show_aorai_state state _args =
+let show_val fmt (expr, v, _) =
+  Format.fprintf fmt "%a in %a"
+    Printer.pp_exp expr
+    (Cvalue.V.pretty_typ (Some (Cil.typeOf expr))) v
+
+let builtin_show_aorai_state state args =
   let history = Data_for_aorai.(curState :: (whole_history ())) in
   Aorai_option.result ~current:true "@[<hv>%a@]"
     (Pretty_utils.pp_list ~sep:" <- " (show_aorai_variable state)) history;
+  if args <> [] then begin
+    Aorai_option.result ~current:true "@[<hv>%a@]"
+      (Pretty_utils.pp_list ~sep:"," show_val) args
+  end;
   (* Return value : returns nothing, changes nothing *)
   {
     Value_types.c_values = [None, state];
@@ -46,8 +55,14 @@ let builtin_show_aorai_state state _args =
     c_cacheable = Value_types.Cacheable;
   }
 
+let show_aorai_state = "Frama_C_show_aorai_state"
+
+let () =
+  Cil_builtins.add_custom_builtin
+    (fun () -> (show_aorai_state,Cil.voidType,[],true))
+
 let () =
-  !Db.Value.register_builtin "Frama_C_show_aorai_state" builtin_show_aorai_state
+  !Db.Value.register_builtin show_aorai_state builtin_show_aorai_state
 
 let add_slevel_annotation vi kind =
   match kind with

tests/libc/oracle/fc_libc.2.res.oracle

@@ -42,7 +42,6 @@ skipping share/libc/__fc_machdep_linux_shared.h
 [kernel] Parsing share/libc/__fc_select.h (with preprocessing)
 [kernel] Parsing share/libc/__fc_string_axiomatic.h (with preprocessing)
 [kernel] Parsing share/libc/alloca.h (with preprocessing)
-[kernel] Parsing share/libc/aorai/aorai.h (with preprocessing)
 [kernel] Parsing share/libc/arpa/inet.h (with preprocessing)
 [kernel] Parsing share/libc/assert.h (with preprocessing)
 [kernel] Parsing share/libc/byteswap.h (with preprocessing)

tests/libc/oracle/fc_libc.5.res.oracle

 #include "__fc_integer.h"
-#include "aorai/aorai.h"

tests/syntax/oracle/bts1553_2.res.oracle

@@ -5,6 +5,8 @@
   struct a {
      int b ;
   };
+  /* compiler builtin: 
+     void Frama_C_show_aorai_state(...);   */
   /* compiler builtin: 
      __builtin_va_list __builtin_next_arg(void);   */
   /* compiler builtin: 
@@ -40,6 +42,8 @@
   struct a {
      int b ;
   };
+  /* compiler builtin: 
+     void Frama_C_show_aorai_state(...);   */
   /* compiler builtin: 
      __builtin_va_list __builtin_next_arg(void);   */
   /* compiler builtin: 

tests/syntax/oracle/check_builtin_bts1440.res.oracle

@@ -2,6 +2,8 @@
 [kernel:file:print-one] 
   result of parsing tests/syntax/check_builtin_bts1440.i:
   /* Generated by Frama-C */
+  void Frama_C_show_aorai_state(...);
+  
   void __builtin__Exit(int);
   
   int __builtin___fprintf_chk(void *, int, char const * , ...);

tests/syntax/oracle/static_formals_1.res.oracle

 [kernel] Parsing tests/syntax/static_formals_1.c (with preprocessing)
 [kernel] Parsing tests/syntax/static_formals_2.c (with preprocessing)
 /* Generated by Frama-C */
-/*@ requires /* vid:25, lvid:25 */x < 10; */
-static int /* vid:58 */f(int /* vid:25, lvid:25 */x);
+/*@ requires /* vid:26, lvid:26 */x < 10; */
+static int /* vid:60 */f(int /* vid:26, lvid:26 */x);
 
-int /* vid:30 */g(void)
+int /* vid:31 */g(void)
 {
-  int /* vid:31 */tmp;
-  /* vid:31 */tmp = /* vid:58 */f(4);
-  return /* vid:31 */tmp;
+  int /* vid:32 */tmp;
+  /* vid:32 */tmp = /* vid:60 */f(4);
+  return /* vid:32 */tmp;
 }
 
-/*@ requires /* vid:53, lvid:53 */x < 10; */
-static int /* vid:59 */f_0(int /* vid:53, lvid:53 */x);
+/*@ requires /* vid:55, lvid:55 */x < 10; */
+static int /* vid:61 */f_0(int /* vid:55, lvid:55 */x);
 
-int /* vid:56 */h(void)
+int /* vid:58 */h(void)
 {
-  int /* vid:57 */tmp;
-  /* vid:57 */tmp = /* vid:59 */f_0(6);
-  return /* vid:57 */tmp;
+  int /* vid:59 */tmp;
+  /* vid:59 */tmp = /* vid:61 */f_0(6);
+  return /* vid:59 */tmp;
 }