From 77142038cd38d2ae87854ecbfcca4b700fd5be69 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 11 Dec 2020 17:09:15 +0100
Subject: [PATCH] [tests] oracles: empty struct refused by default
---
tests/crowbar/complete_type.ml | 8 +--
tests/crowbar/mutable.ml | 6 +-
tests/crowbar/offset_anonymous_field.ml | 2 +-
tests/rte/initialized_union.c | 15 ++--
.../rte/oracle/initialized_union.0.res.oracle | 70 +++++++++++++++++++
....oracle => initialized_union.1.res.oracle} | 0
tests/value/empty_struct2.c | 4 ++
tests/value/oracle/empty_base.1.res.oracle | 2 +
tests/value/oracle/empty_struct.3.res.oracle | 13 ++--
tests/value/oracle/empty_struct.4.res.oracle | 34 ++-------
tests/value/oracle/empty_struct2.res.oracle | 36 +++++-----
11 files changed, 124 insertions(+), 66 deletions(-)
create mode 100644 tests/rte/oracle/initialized_union.0.res.oracle
rename tests/rte/oracle/{initialized_union.res.oracle => initialized_union.1.res.oracle} (100%)
diff --git a/tests/crowbar/complete_type.ml b/tests/crowbar/complete_type.ml
index ecb71403568..5a6a8f18c90 100644
--- a/tests/crowbar/complete_type.ml
+++ b/tests/crowbar/complete_type.ml
@@ -58,12 +58,12 @@ let mk_comp_type
in
let mk_fields compinfo =
match nb_fields with
- | 0 -> compinfo.cdefined <- false; []
- | 1 -> compinfo.cdefined <- true; [ mk_field typ1 ]
- | _ -> compinfo.cdefined <- true; [ mk_field typ1; mk_field typ2 ]
+ | 0 -> None
+ | 1 -> Some [ mk_field typ1 ]
+ | _ -> Some [ mk_field typ1; mk_field typ2 ]
in
let compinfo =
- Cil.mkCompInfo cstruct (type_name()) mk_fields []
+ Cil_const.mkCompInfo cstruct (type_name()) mk_fields []
in
let kind =
match cstruct, nb_fields, kind1, kind2 with
diff --git a/tests/crowbar/mutable.ml b/tests/crowbar/mutable.ml
index 51db8a6fc68..2ce2ae6d599 100644
--- a/tests/crowbar/mutable.ml
+++ b/tests/crowbar/mutable.ml
@@ -39,9 +39,9 @@ let mk_type ftype attr =
let tname = struct_name () in
let fname = field_name () in
let mk_type _ =
- [ fname, ftype, None, attr, Cil_datatype.Location.unknown ]
+ Some [ fname, ftype, None, attr, Cil_datatype.Location.unknown ]
in
- Cil.mkCompInfo true tname ~norig:tname mk_type []
+ Cil_const.mkCompInfo true tname ~norig:tname mk_type []
let mk_int_type field_kind =
let field_attr = attr_of_kind field_kind in
@@ -144,5 +144,5 @@ let test (types, kind) =
end;
true
-let () = Crowbar.add_test ~name:"mutable typeOffset" [ gen_type ] @@
+let () = Crowbar.add_test ~name:"mutable typeOffset" [ gen_type ] @@
(fun x -> Crowbar.check (test x))
diff --git a/tests/crowbar/offset_anonymous_field.ml b/tests/crowbar/offset_anonymous_field.ml
index 15b7277f26d..a5357631574 100644
--- a/tests/crowbar/offset_anonymous_field.ml
+++ b/tests/crowbar/offset_anonymous_field.ml
@@ -24,7 +24,7 @@ let struct_name =
let mk_compinfo cstruct field1 field2 field3 =
let tname = struct_name () in
- let mk_type _ = [ field1; field2; field3 ] in
+ let mk_type _ = Some [ field1; field2; field3 ] in
Cil.mkCompInfo cstruct tname ~norig:tname mk_type []
type result =
diff --git a/tests/rte/initialized_union.c b/tests/rte/initialized_union.c
index ce50aec121a..9f7b960688c 100644
--- a/tests/rte/initialized_union.c
+++ b/tests/rte/initialized_union.c
@@ -1,5 +1,6 @@
/* run.config
OPT: -rte -rte-initialized -warn-signed-overflow -print
+ OPT: -cpp-extra-args="-DEMPTY" -machdep gcc_x86_64 -rte -rte-initialized -warn-signed-overflow -print
*/
union U {
@@ -23,10 +24,10 @@ struct S {
};
union U u_global;
-
+#ifdef EMPTY
// supported by Frama-C
union empty {};
-
+#endif
int main(){
union U u_local1;
@@ -37,9 +38,9 @@ int main(){
union U3 u3_local1;
union U3 u3_local2;
-
+#ifdef EMPTY
union empty e;
-
+#endif
u_local1.c = 1;
u_local2 = u_local1;
@@ -53,12 +54,12 @@ int main(){
u3_local2 = u3_local1;
double f = u_global.f;
-
+
struct S s1, s2;
s1.u.c = 'a';
s2.u = s1.u;
-
+#ifdef EMPTY
union empty e1 = e;
-
+#endif
return 0;
}
diff --git a/tests/rte/oracle/initialized_union.0.res.oracle b/tests/rte/oracle/initialized_union.0.res.oracle
new file mode 100644
index 00000000000..550af6851ce
--- /dev/null
+++ b/tests/rte/oracle/initialized_union.0.res.oracle
@@ -0,0 +1,70 @@
+[kernel] Parsing tests/rte/initialized_union.c (with preprocessing)
+[rte] annotating function main
+/* Generated by Frama-C */
+union U {
+ char c ;
+ int i ;
+ double f ;
+};
+union U2 {
+ int i1 ;
+ int i2 ;
+};
+union U3 {
+ union U u ;
+ union U2 u2 ;
+};
+struct S {
+ union U u ;
+};
+union U u_global;
+int main(void)
+{
+ int __retres;
+ union U u_local1;
+ union U u_local2;
+ union U2 u2_local1;
+ union U2 u2_local2;
+ union U3 u3_local1;
+ union U3 u3_local2;
+ struct S s1;
+ struct S s2;
+ u_local1.c = (char)1;
+ /*@ assert
+ rte: initialization_of_union:
+ \initialized(&u_local1.c) ∨ \initialized(&u_local1.i) ∨
+ \initialized(&u_local1.f);
+ */
+ u_local2 = u_local1;
+ /*@ assert rte: initialization: \initialized(&u_local1.i); */
+ u2_local1.i2 = u_local1.i;
+ /*@ assert
+ rte: initialization_of_union:
+ \initialized(&u2_local1.i1) ∨ \initialized(&u2_local1.i2);
+ */
+ u2_local2 = u2_local1;
+ /*@ assert
+ rte: initialization_of_union:
+ \initialized(&u_local1.c) ∨ \initialized(&u_local1.i) ∨
+ \initialized(&u_local1.f);
+ */
+ u3_local1.u = u_local1;
+ /*@ assert
+ rte: initialization_of_union:
+ \initialized(&u3_local1.u) ∨ \initialized(&u3_local1.u2);
+ */
+ u3_local2 = u3_local1;
+ double f = u_global.f;
+ s1.u.c = (char)'a';
+ /*@ assert
+ rte: initialization_of_union:
+ \initialized(&s1.u.c) ∨ \initialized(&s1.u.i) ∨
+ \initialized(&s1.u.f);
+ */
+ s2.u = s1.u;
+ __retres = 0;
+ /*@ assert rte: initialization: \initialized(&__retres); */
+ return __retres;
+}
+
+
diff --git a/tests/rte/oracle/initialized_union.res.oracle b/tests/rte/oracle/initialized_union.1.res.oracle
similarity index 100%
rename from tests/rte/oracle/initialized_union.res.oracle
rename to tests/rte/oracle/initialized_union.1.res.oracle
diff --git a/tests/value/empty_struct2.c b/tests/value/empty_struct2.c
index 857b049965c..9cff3b7e350 100644
--- a/tests/value/empty_struct2.c
+++ b/tests/value/empty_struct2.c
@@ -1,3 +1,7 @@
+/* run.config
+ STDOPT: +"-machdep gcc_x86_64"
+*/
+
#include <string.h>
volatile int nondet;
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/value/oracle/empty_base.1.res.oracle
index 5a745e4a9df..421cd027e05 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/value/empty_base.c (with preprocessing)
+[kernel] tests/value/empty_base.c:12: User Error:
+ Empty struct is allowed only in GCC or MSVC mode
[kernel] tests/value/empty_base.c:47: User Error:
zero-length arrays only allowed for GCC/MSVC
[kernel] tests/value/empty_base.c:49: User Error:
diff --git a/tests/value/oracle/empty_struct.3.res.oracle b/tests/value/oracle/empty_struct.3.res.oracle
index f829aaf782e..e0e86c212af 100644
--- a/tests/value/oracle/empty_struct.3.res.oracle
+++ b/tests/value/oracle/empty_struct.3.res.oracle
@@ -1,7 +1,8 @@
[kernel] Parsing tests/value/empty_struct.c (with preprocessing)
-[eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] tests/value/empty_struct.c:22: User Error:
- empty structs are unsupported (type 'struct s', location s)
- in C99 (only allowed as GCC/MSVC extension). Aborting.
-[kernel] Plug-in eva aborted: invalid user input.
+[kernel] tests/value/empty_struct.c:13: User Error:
+ Empty struct is allowed only in GCC or MSVC mode
+[kernel] tests/value/empty_struct.c:67: User Error:
+ Empty struct is allowed only in GCC or MSVC mode
+[kernel] User Error: stopping on file "tests/value/empty_struct.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/empty_struct.4.res.oracle b/tests/value/oracle/empty_struct.4.res.oracle
index 62bc2e7b1de..e0e86c212af 100644
--- a/tests/value/oracle/empty_struct.4.res.oracle
+++ b/tests/value/oracle/empty_struct.4.res.oracle
@@ -1,28 +1,8 @@
[kernel] Parsing tests/value/empty_struct.c (with preprocessing)
-[eva] Analyzing a complete application starting at main2
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- NULL[rbits 0 to 15] ∈ [--..--]
- s2 ∈ {0}
- pgs ∈ {{ &gs }}
-[eva:alarm] tests/value/empty_struct.c:70: Warning:
- out of bounds read. assert \valid_read(ptr_ret);
-[eva] Recording results for main2
-[eva] done for function main2
-[eva] tests/value/empty_struct.c:70:
- assertion 'Eva,mem_access' got final status invalid.
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main2:
- ptr_ret ∈ {2}
-[from] Computing for function main2
-[from] Done for function main2
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main2:
- NO EFFECTS
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main2:
- ptr_ret
-[inout] Inputs for function main2:
- \nothing
+[kernel] tests/value/empty_struct.c:13: User Error:
+ Empty struct is allowed only in GCC or MSVC mode
+[kernel] tests/value/empty_struct.c:67: User Error:
+ Empty struct is allowed only in GCC or MSVC mode
+[kernel] User Error: stopping on file "tests/value/empty_struct.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/empty_struct2.res.oracle b/tests/value/oracle/empty_struct2.res.oracle
index f1dc97624c7..ce834bb8c23 100644
--- a/tests/value/oracle/empty_struct2.res.oracle
+++ b/tests/value/oracle/empty_struct2.res.oracle
@@ -5,43 +5,43 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
pg ∈ {{ &global_empty }}
-[eva] tests/value/empty_struct2.c:44: assertion got status valid.
-[eva] tests/value/empty_struct2.c:46: Frama_C_show_each_global_empty: ∅
-[eva] tests/value/empty_struct2.c:47: Frama_C_show_each_e1: ∅
-[eva] tests/value/empty_struct2.c:48: Call to builtin memcpy
-[eva] tests/value/empty_struct2.c:48:
+[eva] tests/value/empty_struct2.c:48: assertion got status valid.
+[eva] tests/value/empty_struct2.c:50: Frama_C_show_each_global_empty: ∅
+[eva] tests/value/empty_struct2.c:51: Frama_C_show_each_e1: ∅
+[eva] tests/value/empty_struct2.c:52: Call to builtin memcpy
+[eva] tests/value/empty_struct2.c:52:
function memcpy: precondition 'valid_dest' got status valid.
-[eva] tests/value/empty_struct2.c:48:
+[eva] tests/value/empty_struct2.c:52:
function memcpy: precondition 'valid_src' got status valid.
-[eva] tests/value/empty_struct2.c:48:
+[eva] tests/value/empty_struct2.c:52:
function memcpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:98:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-[eva] tests/value/empty_struct2.c:53: Call to builtin memcpy
-[eva] tests/value/empty_struct2.c:53:
+[eva] tests/value/empty_struct2.c:57: Call to builtin memcpy
+[eva] tests/value/empty_struct2.c:57:
function memcpy: precondition 'valid_dest' got status valid.
-[eva] tests/value/empty_struct2.c:53:
+[eva] tests/value/empty_struct2.c:57:
function memcpy: precondition 'valid_src' got status valid.
-[eva] tests/value/empty_struct2.c:53:
+[eva] tests/value/empty_struct2.c:57:
function memcpy: precondition 'separation' got status valid.
-[eva] tests/value/empty_struct2.c:54:
+[eva] tests/value/empty_struct2.c:58:
Frama_C_show_each_c2: .a ∈ {42}
.b ∈ {77}
-[eva] tests/value/empty_struct2.c:55: Frama_C_show_each_c2_e: ∅
+[eva] tests/value/empty_struct2.c:59: Frama_C_show_each_c2_e: ∅
[eva] computing for function f <- main.
- Called from tests/value/empty_struct2.c:56.
+ Called from tests/value/empty_struct2.c:60.
[eva] Recording results for f
[eva] Done for function f
-[eva] tests/value/empty_struct2.c:58:
+[eva] tests/value/empty_struct2.c:62:
Frama_C_show_each_res: .a ∈ {87}
.b ∈ {39}
-[eva] tests/value/empty_struct2.c:62: assertion got status valid.
+[eva] tests/value/empty_struct2.c:66: assertion got status valid.
[eva] computing for function ret_empty <- main.
- Called from tests/value/empty_struct2.c:64.
+ Called from tests/value/empty_struct2.c:68.
[eva] using specification for function ret_empty
[eva] Done for function ret_empty
[eva] computing for function ret_ptr_empty <- main.
- Called from tests/value/empty_struct2.c:65.
+ Called from tests/value/empty_struct2.c:69.
[eva] using specification for function ret_ptr_empty
[eva] Done for function ret_ptr_empty
[eva] Recording results for main
--
GitLab