From be0ed8aa9eb1dfd6a2001d3d0de6f247c5fdbadd Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 29 Aug 2019 18:09:55 +0200
Subject: [PATCH] [tests] remove directory 'reject'
---
src/plugins/e-acsl/Makefile.in | 1 -
.../tests/reject/function_declaration.i | 16 --
.../oracle/function_declaration.err.oracle | 0
.../oracle/function_declaration.res.oracle | 142 ------------------
.../tests/reject/oracle/quantif.res.oracle | 48 ------
src/plugins/e-acsl/tests/reject/quantif.i | 18 ---
.../e-acsl/tests/reject/result/.gitkeep | 0
src/plugins/e-acsl/tests/reject/test_config | 1 -
8 files changed, 226 deletions(-)
delete mode 100644 src/plugins/e-acsl/tests/reject/function_declaration.i
delete mode 100644 src/plugins/e-acsl/tests/reject/oracle/function_declaration.err.oracle
delete mode 100644 src/plugins/e-acsl/tests/reject/oracle/function_declaration.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/reject/quantif.i
delete mode 100644 src/plugins/e-acsl/tests/reject/result/.gitkeep
delete mode 100644 src/plugins/e-acsl/tests/reject/test_config
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 61491fcb533..cc38e19deb7 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -180,7 +180,6 @@ else
PLUGIN_TESTS_DIRS := \
format \
- reject \
runtime \
bts \
gmp \
diff --git a/src/plugins/e-acsl/tests/reject/function_declaration.i b/src/plugins/e-acsl/tests/reject/function_declaration.i
deleted file mode 100644
index 52b84515f23..00000000000
--- a/src/plugins/e-acsl/tests/reject/function_declaration.i
+++ /dev/null
@@ -1,16 +0,0 @@
-/* run.config
- DONTRUN:
- COMMENT: function declaration with a contract
- COMMENT: does not work, but yet for a bad reason
- COMMENT: (assigns \nothing generated and not yet supported)
-*/
-
-int X = 0;
-
-/*@ requires X == 0; */
-void f(void);
-
-int main(void) {
- f();
- return 0;
-}
diff --git a/src/plugins/e-acsl/tests/reject/oracle/function_declaration.err.oracle b/src/plugins/e-acsl/tests/reject/oracle/function_declaration.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/reject/oracle/function_declaration.res.oracle b/src/plugins/e-acsl/tests/reject/oracle/function_declaration.res.oracle
deleted file mode 100644
index 7430ba81f30..00000000000
--- a/src/plugins/e-acsl/tests/reject/oracle/function_declaration.res.oracle
+++ /dev/null
@@ -1,142 +0,0 @@
-tests/reject/function_declaration.i:7:[kernel] failure: You used visitCilFileSameGlobals but the global got changed:
- int X = 0;
-
- changed to
- /*************/
- /* GMP types */
- /*************/
-
- typedef struct {
- int _mp_alloc;
- int _mp_size;
- unsigned long int *_mp_d;
- } __mpz_struct;
-
- typedef __mpz_struct mpz_t[1];
-
- /*****************/
- /* GMP functions */
- /*****************/
-
- // initilializers
-
- /*@ ensures \valid(x);
- @ assigns *x; */
- extern void mpz_init(mpz_t x);
-
- /*@ ensures \valid(z);
- @ assigns *z; */
- extern void mpz_init_set_ui(mpz_t z, unsigned long int n);
-
- /*@ ensures \valid(z);
- @ assigns *z; */
- extern void mpz_init_set_si(mpz_t z, signed long int n);
-
- /*@ ensures \valid(z);
- @ assigns *z; */
- extern int mpz_init_set_str(mpz_t z, const char *str, int base);
-
- // finalizer
-
- /*@ requires \valid(x);
- @ assigns *x; */
- extern void mpz_clear(mpz_t x);
-
- // logical and arithmetic operators
-
- /*@ requires \valid(z1);
- @ requires \valid(z2);
- @ assigns \nothing; */
- extern int mpz_cmp(const mpz_t z1, const mpz_t z2);
-
- /*@ requires \valid(z1);
- @ requires \valid(z2);
- @ assigns *z1; */
- extern int mpz_comp(mpz_t z1, const mpz_t z2);
-
- /*@ requires \valid(z1);
- @ requires \valid(z2);
- @ assigns *z1; */
- extern void mpz_neg(mpz_t z1, const mpz_t z2);
-
- /*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
- @ assigns *z1; */
- extern void mpz_add(mpz_t z1, const mpz_t z2, const mpz_t z3);
-
- /*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
- @ assigns *z1; */
- extern void mpz_sub(mpz_t z1, const mpz_t z2, const mpz_t z3);
-
- /*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
- @ assigns *z1; */
- extern void mpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3);
-
- /*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
- @ assigns *z1; */
- extern void mpz_cdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3);
-
- /*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
- @ assigns *z1; */
- extern void mpz_mod(mpz_t z1, const mpz_t z2, const mpz_t z3);
- // TODO: remplacer par un e_acsl.h.in
- // faire générer par le makefile un e_acsl.h
- // avec des #include "FRAMAC_SHARE/libc/stdio.h", etc
-
- // [TODO] ne pas générer les typedef si on veut linker avec GMP derrière
-
- // [TODO] utiliser un champ modèle de type integer pour modéliser
- // l'entier exact correspondant à un mpz_t.
- // Not yet implemented in ACSL.
-
- /************************/
- /* Standard C functions */
- /************************/
-
- /*@ terminates \false;
- @ assigns \nothing;
- @ ensures \false; */
- extern void exit(int status);
-
- /*@ assigns \nothing; */
- extern int printf(const char *, ...);
-
- /*****************************/
- /* Dedicated E-ACSL function */
- /*****************************/
-
- void e_acsl_fail(char *msg) { printf("%s\n", msg); exit(1); }
-
-
- int X = 0;
-[kernel] The full backtrace is:
- Raised at file "src/kernel/log.ml", line 509, characters 30-31
- Called from file "src/kernel/log.ml", line 503, characters 2-9
- Re-raised at file "src/kernel/log.ml", line 506, characters 8-9
- Called from file "list.ml", line 69, characters 12-15
- Called from file "cil/src/cil.ml", line 7969, characters 3-30
- Called from file "cil/src/cil.ml", line 8013, characters 2-368
- Called from file "cil/src/cil.ml", line 6380, characters 21-41
- Called from file "cil/src/cil.ml", line 8044, characters 7-84
- Called from file "src/kernel/visitor.ml", line 299, characters 2-45
- Called from file "src/type/type.ml", line 600, characters 39-44
- Called from file "queue.ml", line 134, characters 6-20
- Called from file "src/kernel/boot.ml", line 36, characters 4-20
- Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
- Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
-
- Frama-C aborted because of internal error.
- Please report as 'crash' at http://bts.frama-c.com/.
- Your Frama-C version is Carbon-20110201+dev.
- Note that a version and a backtrace alone often does not have information
- to understand the bug. Guidelines for reporting bugs are at:
- http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
diff --git a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
deleted file mode 100644
index e0703e776a6..00000000000
--- a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
+++ /dev/null
@@ -1,48 +0,0 @@
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing tests/reject/quantif.i (no preprocessing)
-[e-acsl] tests/reject/quantif.i:6: Warning:
- E-ACSL construct `unguarded \forall quantification' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:7: Warning:
- invalid E-ACSL construct
- `invalid guard x ≡ 1 in quantification ∀ ℤ x; x ≡ 1 ⇒ x ≥ 0'.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:8: Warning:
- invalid E-ACSL construct
- `missing upper-bound for variable x in quantification ∀ int x; 0 ≤ x ⇒ x ≥ 0'.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:9: Warning:
- invalid E-ACSL construct
- `non integer variable x in quantification ∀ float x; 0 ≤ x ≤ 3 ⇒ x ≥ 0'.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:10: Warning:
- invalid E-ACSL construct
- `unguarded variable y in quantification
- ∀ ℤ x, ℤ y; 0 ≤ x ≤ 3 ⇒ x ≥ 0'.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:11: Warning:
- invalid E-ACSL construct
- `too much constraint(s) in quantification ∀ ℤ x; 0 ≤ x ≤ 3 ∧ 0 ≤ z ≤ 3 ⇒ x ≥ 0'.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:12: Warning:
- invalid E-ACSL construct
- `invalid guard (0 ≤ x ≤ 3) ∨ (0 ≤ y ≤ 3) in quantification
- ∀ ℤ x, ℤ y; (0 ≤ x ≤ 3) ∨ (0 ≤ y ≤ 3) ⇒ x ≥ 0'.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:13: Warning:
- invalid E-ACSL construct
- `invalid binder x + 1 in quantification ∀ int x; 0 ≤ x + 1 ≤ 3 ⇒ x ≥ 0'.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:14: Warning:
- invalid E-ACSL construct
- `too much constraint(s) in quantification ∀ ℤ x; 0 ≤ x < 10 ∧ 9 ≤ x < 20 ⇒ x > z'.
- Ignoring annotation.
-[e-acsl] tests/reject/quantif.i:15: Warning:
- invalid E-ACSL construct
- `invalid binder y in quantification
- ∀ ℤ x, ℤ z, ℤ y;
- 0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x + z ≤ y + 1'.
- Ignoring annotation.
-[e-acsl] 9 annotations were ignored, being untypable.
-[e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/tests/reject/quantif.i b/src/plugins/e-acsl/tests/reject/quantif.i
deleted file mode 100644
index 399d330d0ea..00000000000
--- a/src/plugins/e-acsl/tests/reject/quantif.i
+++ /dev/null
@@ -1,18 +0,0 @@
-/* run.config
- COMMENT: invalid quantifications */
-
-int main(void) {
- int z;
- /*@ assert \forall integer x; x >= 0; */
- /*@ assert \forall integer x; x == 1 ==> x >= 0; */
- /*@ assert \forall int x; 0 <= x ==> x >= 0; */
- /*@ assert \forall float x; 0 <= x <= 3 ==> x >= 0; */
- /*@ assert \forall integer x,y; 0 <= x <= 3 ==> x >= 0; */
- /*@ assert \forall integer x; 0 <= x <= 3 && 0 <= z <= 3 ==> x >= 0; */
- /*@ assert \forall integer x,y; 0 <= x <= 3 || 0 <= y <= 3 ==> x >= 0; */
- /*@ assert \forall int x; 0 <= x+1 <= 3 ==> x >= 0; */
- /*@ assert \forall integer x; 0 <= x < 10 && 9 <= x < 20 ==> x > z; */
- /*@ assert \forall integer x,z,y; 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y
- ==> x+z <= y+1; */
- return 0;
-}
diff --git a/src/plugins/e-acsl/tests/reject/result/.gitkeep b/src/plugins/e-acsl/tests/reject/result/.gitkeep
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/reject/test_config b/src/plugins/e-acsl/tests/reject/test_config
deleted file mode 100644
index 61e3a7b0e53..00000000000
--- a/src/plugins/e-acsl/tests/reject/test_config
+++ /dev/null
@@ -1 +0,0 @@
-OPT: -e-acsl-check
--
GitLab