From 550e55596e1491155a15280cd1cc27f3a38959ec Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 19 Aug 2019 14:56:58 +0200
Subject: [PATCH] [Tests] Moves an old test related to makeFormalVar in the
right dir and add a new test related to ghost parameters
---
tests/{misc => cil}/Change_formals.ml | 0
tests/cil/change_formals.c | 17 +++
tests/cil/insert_formal.i | 103 ++++++++++++++++++
tests/cil/insert_formal.ml | 53 +++++++++
.../oracle/change_formals.0.res.oracle | 2 +-
.../oracle/change_formals.1.res.oracle | 2 +-
.../oracle/change_formals.2.res.oracle | 2 +-
tests/cil/oracle/insert_formal.res.oracle | 103 ++++++++++++++++++
tests/misc/change_formals.c | 17 ---
9 files changed, 279 insertions(+), 20 deletions(-)
rename tests/{misc => cil}/Change_formals.ml (100%)
create mode 100644 tests/cil/change_formals.c
create mode 100644 tests/cil/insert_formal.i
create mode 100644 tests/cil/insert_formal.ml
rename tests/{misc => cil}/oracle/change_formals.0.res.oracle (75%)
rename tests/{misc => cil}/oracle/change_formals.1.res.oracle (69%)
rename tests/{misc => cil}/oracle/change_formals.2.res.oracle (77%)
create mode 100644 tests/cil/oracle/insert_formal.res.oracle
delete mode 100644 tests/misc/change_formals.c
diff --git a/tests/misc/Change_formals.ml b/tests/cil/Change_formals.ml
similarity index 100%
rename from tests/misc/Change_formals.ml
rename to tests/cil/Change_formals.ml
diff --git a/tests/cil/change_formals.c b/tests/cil/change_formals.c
new file mode 100644
index 00000000000..5ac6f89b75e
--- /dev/null
+++ b/tests/cil/change_formals.c
@@ -0,0 +1,17 @@
+/* run.config
+EXECNOW: make -s tests/cil/Change_formals.cmxs
+OPT: -load-module tests/cil/Change_formals.cmxs -cpp-extra-args="-DNO_PROTO" -then-on test -print
+OPT: -load-module tests/cil/Change_formals.cmxs -cpp-extra-args="-DNO_IMPLEM" -then-on test -print
+OPT: -load-module tests/cil/Change_formals.cmxs -then-on test -print
+*/
+
+#ifndef NO_PROTO
+int f(int x);
+#endif
+
+#ifndef NO_IMPLEM
+int f(int x) { return x; }
+#endif
+
+// needed to prevent erasure of f in NO_IMPLEM case
+int g() { return f(0); }
diff --git a/tests/cil/insert_formal.i b/tests/cil/insert_formal.i
new file mode 100644
index 00000000000..5076f1f5c89
--- /dev/null
+++ b/tests/cil/insert_formal.i
@@ -0,0 +1,103 @@
+/* run.config
+OPT: -load-script tests/cil/insert_formal.ml -print
+*/
+
+// v
+void void_circumflex( void ) {
+
+}
+
+// v
+void void_circumflex_g( void ) {
+
+}
+
+// v
+void void_dollar( void ) {
+
+}
+
+// v
+void void_dollar_g( void ) {
+
+}
+
+// v
+void a_circumflex( int a ) {
+
+}
+
+// v
+void a_dollar( int a ) {
+
+}
+
+// v
+void a_circumflex_g( int a ) {
+
+}
+
+// v
+void a_dollar_g( int a ) {
+
+}
+
+// v
+void a_a( int a ){
+
+}
+
+// v
+void ghost_a_circumflex( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void ghost_a_dollar( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void ghost_a_circumflex_g( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void ghost_a_dollar_g( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void ghost_a_a( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void a_b_c_a (int a, int b, int c) {
+
+}
+
+// v
+void b_a_c_a (int b, int a, int c) {
+
+}
+
+// v
+void all_ghost_a_b_c_a ( void )/*@ ghost (int a, int b, int c) */ {
+
+}
+
+// v
+void all_ghost_b_a_c_a ( void )/*@ ghost (int b, int a, int c) */ {
+
+}
+
+// v
+void a_ghost_b_c_a ( int a )/*@ ghost (int b, int c) */ {
+
+}
+
+// v
+void b_ghost_a_c_a ( int b )/*@ ghost (int a, int c) */ {
+
+}
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
new file mode 100644
index 00000000000..dd545df87cc
--- /dev/null
+++ b/tests/cil/insert_formal.ml
@@ -0,0 +1,53 @@
+open Cil_types
+
+class visitor = object
+ inherit Visitor.frama_c_inplace
+
+ method! vfunc f =
+ let insert_circ f = Cil.makeFormalVar f ~where:"^" "x" Cil.intType in
+ let insert_dollar f = Cil.makeFormalVar f ~where:"$" "x" Cil.intType in
+ let insert_circ_g f = Cil.makeFormalVar f ~where:"^g" "x" Cil.intType in
+ let insert_dollar_g f = Cil.makeFormalVar f ~where:"$g" "x" Cil.intType in
+ let insert_a f = Cil.makeFormalVar f ~where:"a" "x" Cil.intType in
+ let circ_list = [
+ "void_circumflex" ;
+ "a_circumflex" ;
+ "ghost_a_circumflex"
+ ] in
+ let dollar_list = [
+ "void_dollar" ;
+ "a_dollar" ;
+ "ghost_a_dollar"
+ ] in
+ let circ_g_list = [
+ "void_circumflex_g" ;
+ "a_circumflex_g" ;
+ "ghost_a_circumflex_g"
+ ] in
+ let dollar_g_list = [
+ "void_dollar_g" ;
+ "a_dollar_g" ;
+ "ghost_a_dollar_g"
+ ] in
+ let a_list = [
+ "a_a" ;
+ "ghost_a_a" ;
+ "a_b_c_a" ;
+ "b_a_c_a" ;
+ "all_ghost_a_b_c_a" ;
+ "all_ghost_b_a_c_a" ;
+ "a_ghost_b_c_a" ;
+ "b_ghost_a_c_a"
+ ] in
+ if List.mem f.svar.vname circ_list then ignore(insert_circ f) ;
+ if List.mem f.svar.vname dollar_list then ignore(insert_dollar f) ;
+ if List.mem f.svar.vname circ_g_list then ignore(insert_circ_g f) ;
+ if List.mem f.svar.vname dollar_g_list then ignore(insert_dollar_g f) ;
+ if List.mem f.svar.vname a_list then ignore(insert_a f) ;
+ Cil.DoChildren
+end
+
+let run () =
+ Visitor.visitFramacFileSameGlobals (new visitor) (Ast.get ())
+
+let () = Db.Main.extend run
diff --git a/tests/misc/oracle/change_formals.0.res.oracle b/tests/cil/oracle/change_formals.0.res.oracle
similarity index 75%
rename from tests/misc/oracle/change_formals.0.res.oracle
rename to tests/cil/oracle/change_formals.0.res.oracle
index 22dc10f37e8..794634cc91e 100644
--- a/tests/misc/oracle/change_formals.0.res.oracle
+++ b/tests/cil/oracle/change_formals.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
[test] current prj = project "test"
[test] current prj = project "test"
/* Generated by Frama-C */
diff --git a/tests/misc/oracle/change_formals.1.res.oracle b/tests/cil/oracle/change_formals.1.res.oracle
similarity index 69%
rename from tests/misc/oracle/change_formals.1.res.oracle
rename to tests/cil/oracle/change_formals.1.res.oracle
index 1f5fcdcd5e9..0269f038c67 100644
--- a/tests/misc/oracle/change_formals.1.res.oracle
+++ b/tests/cil/oracle/change_formals.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
[test] current prj = project "test"
/* Generated by Frama-C */
int f(int x, int ok);
diff --git a/tests/misc/oracle/change_formals.2.res.oracle b/tests/cil/oracle/change_formals.2.res.oracle
similarity index 77%
rename from tests/misc/oracle/change_formals.2.res.oracle
rename to tests/cil/oracle/change_formals.2.res.oracle
index 3f746d6b7f6..9e91be519b3 100644
--- a/tests/misc/oracle/change_formals.2.res.oracle
+++ b/tests/cil/oracle/change_formals.2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
[test] current prj = project "test"
[test] current prj = project "test"
/* Generated by Frama-C */
diff --git a/tests/cil/oracle/insert_formal.res.oracle b/tests/cil/oracle/insert_formal.res.oracle
new file mode 100644
index 00000000000..935880bfc24
--- /dev/null
+++ b/tests/cil/oracle/insert_formal.res.oracle
@@ -0,0 +1,103 @@
+[kernel] Parsing tests/cil/insert_formal.i (no preprocessing)
+/* Generated by Frama-C */
+void void_circumflex(int x)
+{
+ return;
+}
+
+void void_circumflex_g(void)/*@ ghost (int x) */
+{
+ return;
+}
+
+void void_dollar(int x)
+{
+ return;
+}
+
+void void_dollar_g(void)/*@ ghost (int x) */
+{
+ return;
+}
+
+void a_circumflex(int x, int a)
+{
+ return;
+}
+
+void a_dollar(int a, int x)
+{
+ return;
+}
+
+void a_circumflex_g(int a)/*@ ghost (int x) */
+{
+ return;
+}
+
+void a_dollar_g(int a)/*@ ghost (int x) */
+{
+ return;
+}
+
+void a_a(int a, int x)
+{
+ return;
+}
+
+void ghost_a_circumflex(int x)/*@ ghost (int a) */
+{
+ return;
+}
+
+void ghost_a_dollar(int x)/*@ ghost (int a) */
+{
+ return;
+}
+
+void ghost_a_circumflex_g(void)/*@ ghost (int x, int a) */
+{
+ return;
+}
+
+void ghost_a_dollar_g(void)/*@ ghost (int a, int x) */
+{
+ return;
+}
+
+void ghost_a_a(void)/*@ ghost (int a, int x) */
+{
+ return;
+}
+
+void a_b_c_a(int a, int x, int b, int c)
+{
+ return;
+}
+
+void b_a_c_a(int b, int a, int x, int c)
+{
+ return;
+}
+
+void all_ghost_a_b_c_a(void)/*@ ghost (int a, int x, int b, int c) */
+{
+ return;
+}
+
+void all_ghost_b_a_c_a(void)/*@ ghost (int b, int a, int x, int c) */
+{
+ return;
+}
+
+void a_ghost_b_c_a(int a, int x)/*@ ghost (int b, int c) */
+{
+ return;
+}
+
+void b_ghost_a_c_a(int b)/*@ ghost (int a, int x, int c) */
+{
+ return;
+}
+
+
diff --git a/tests/misc/change_formals.c b/tests/misc/change_formals.c
deleted file mode 100644
index c84ec7afade..00000000000
--- a/tests/misc/change_formals.c
+++ /dev/null
@@ -1,17 +0,0 @@
-/* run.config
-EXECNOW: make -s tests/misc/Change_formals.cmxs
-OPT: -load-module tests/misc/Change_formals.cmxs -cpp-extra-args="-DNO_PROTO" -then-on test -print
-OPT: -load-module tests/misc/Change_formals.cmxs -cpp-extra-args="-DNO_IMPLEM" -then-on test -print
-OPT: -load-module tests/misc/Change_formals.cmxs -then-on test -print
-*/
-
-#ifndef NO_PROTO
-int f(int x);
-#endif
-
-#ifndef NO_IMPLEM
-int f(int x) { return x; }
-#endif
-
-// needed to prevent erasure of f in NO_IMPLEM case
-int g() { return f(0); }
--
GitLab