From e6422723eb0bb0cfe8596bc2001256c377917b52 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 7 Jan 2021 16:03:01 +0100
Subject: [PATCH] [aorai] register Frama_C_aorai_show_state as builtin
---
.../aorai/aorai_eva_analysis.enabled.ml | 19 +++++++++++++--
tests/libc/oracle/fc_libc.2.res.oracle | 1 -
tests/libc/oracle/fc_libc.5.res.oracle | 1 -
tests/syntax/oracle/bts1553_2.res.oracle | 4 ++++
.../oracle/check_builtin_bts1440.res.oracle | 2 ++
.../syntax/oracle/static_formals_1.res.oracle | 24 +++++++++----------
6 files changed, 35 insertions(+), 16 deletions(-)
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 007c6ed88fe..5b481c60b1d 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/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
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 852a3378808..b1e1247a436 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/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)
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
index 3c89feea03b..73dac90425a 100644
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ b/tests/libc/oracle/fc_libc.5.res.oracle
@@ -1,2 +1 @@
#include "__fc_integer.h"
-#include "aorai/aorai.h"
diff --git a/tests/syntax/oracle/bts1553_2.res.oracle b/tests/syntax/oracle/bts1553_2.res.oracle
index 9293259fe56..93dacee5149 100644
--- a/tests/syntax/oracle/bts1553_2.res.oracle
+++ b/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:
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 510a8f2b3ab..f81e5813ccc 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/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 * , ...);
diff --git a/tests/syntax/oracle/static_formals_1.res.oracle b/tests/syntax/oracle/static_formals_1.res.oracle
index 94353adf96c..f3dc98b3d30 100644
--- a/tests/syntax/oracle/static_formals_1.res.oracle
+++ b/tests/syntax/oracle/static_formals_1.res.oracle
@@ -1,24 +1,24 @@
[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;
}
--
GitLab