Skip to content
Snippets Groups Projects
Commit be0ed8aa authored by Julien Signoles's avatar Julien Signoles
Browse files

[tests] remove directory 'reject'

parent 738c07a7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 226 deletions
src/plugins/e-acsl/Makefile.in
+ 0
− 1
View file @ be0ed8aa
......@@ -180,7 +180,6 @@ else
PLUGIN_TESTS_DIRS := \
format \
reject \
runtime \
bts \
gmp \
......
src/plugins/e-acsl/tests/reject/function_declaration.i deleted 100644 → 0
+ 0
− 16
View file @ 738c07a7
/* 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;
}
src/plugins/e-acsl/tests/reject/oracle/function_declaration.res.oracle deleted 100644 → 0
+ 0
− 142
View file @ 738c07a7
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 gnrer par le makefile un e_acsl.h
// avec des #include "FRAMAC_SHARE/libc/stdio.h", etc
// [TODO] ne pas gnrer les typedef si on veut linker avec GMP derrire
// [TODO] utiliser un champ modle de type integer pour modliser
// 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
src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle deleted 100644 → 0
+ 0
− 48
View file @ 738c07a7
[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.
src/plugins/e-acsl/tests/reject/quantif.i deleted 100644 → 0
+ 0
− 18
View file @ 738c07a7
/* 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;
}
src/plugins/e-acsl/tests/reject/result/.gitkeep deleted 100644 → 0
+ 0
− 0
View file @ 738c07a7
src/plugins/e-acsl/tests/reject/test_config deleted 100644 → 0
+ 0
− 1
View file @ 738c07a7
OPT: -e-acsl-check
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment