Skip to content
Snippets Groups Projects
Commit 8d0d7174 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[Test] adding EXIT directives

parent 81fbd5b4
No related branches found
No related tags found
No related merge requests found
Showing
with 96 additions and 32 deletions
/*@
axiomatic bla1 {
/* run.config*
EXIT: 1
STDOPT:
*/
/*@ axiomatic bla1 {
// nested axiomatics are not allowed
axiomatic bla2 {
predicate bla3{L}(int n);
......
/* run.config
EXIT: 1
STDOPT:
*/
int BadReturn1(int* p) {
*p++;
return;
......@@ -9,7 +12,6 @@ int BadReturn2(int* p) {
return;
}
int main() {
int i = 3;
BadReturn2(&i);
......
/* run.config
EXIT: 0
STDOPT: +"-cpp-command='gcc -C -E -I.'" +"-cpp-frama-c-compliant"
EXIT: 1
STDOPT: +"-cpp-command='gcc -C -E -I. -DERR'" +"-cpp-frama-c-compliant"
*/
int t[4];
#ifdef ERR
int q[static 3];
#endif
......
/* run.config*
EXIT: 1
STDOPT:
*/
int i1 = 10; /* Definition, external linkage */
static int i2 = 20; /* Definition, internal linkage */
extern int i3 = 30; /* Definition, external linkage */
......
/* run.config
STDOPT: +"-cpp-extra-args='-DTEST_ASSERT'"
STDOPT: +"-cpp-extra-args='-DTEST_ERRNO'"
STDOPT: +"-cpp-extra-args='-DTEST_MATHERRHANDLING'"
STDOPT: +"-cpp-extra-args='-DTEST_VASTART'"
STDOPT: +"-cpp-extra-args='-DTEST_VACOPY'"
STDOPT: +"-cpp-extra-args='-DTEST_VAARG'"
STDOPT: +"-cpp-extra-args='-DTEST_VAEND'"
STDOPT: +"-cpp-extra-args='-DTEST_SETJMP'"
EXIT: 1
STDOPT: +"-cpp-extra-args='-DTEST_ASSERT'"
STDOPT : +"-cpp-extra-args='-DTEST_ERRNO'"
STDOPT: +"-cpp-extra-args='-DTEST_MATHERRHANDLING'"
STDOPT: +"-cpp-extra-args='-DTEST_VASTART'"
STDOPT: +"-cpp-extra-args='-DTEST_VACOPY'"
STDOPT: +"-cpp-extra-args='-DTEST_VAARG'"
STDOPT: +"-cpp-extra-args='-DTEST_VAEND'"
STDOPT: +"-cpp-extra-args='-DTEST_SETJMP'"
*/
#include <assert.h>
#include <stdarg.h>
#include <setjmp.h>
#ifdef TEST_ASSERT
typedef void (*handler_type)(int);
void execute_handler(handler_type handler, int value) {
......
/* run.config*
EXIT: 1
STDOPT:
*/
struct s1 { int a; };
struct s2 { int a; };
......
/* run.config
STDOPT:
EXIT:1
STDOPT: +" -cpp-extra-args=-DT0"
STDOPT: +" -cpp-extra-args=-DT1"
STDOPT: +" -cpp-extra-args=-DT2"
STDOPT: +" -cpp-extra-args=-DT3"
STDOPT: +" -cpp-extra-args=-DT4"
STDOPT: +" -cpp-extra-args=-DT5"
EXIT:0
STDOPT: +" -cpp-extra-args=-DT6"
STDOPT: +" -cpp-extra-args=-DT7"
EXIT:1
STDOPT: +" -cpp-extra-args=-DT8"
*/
/* The first run is correct. The others should fail, as they include invalid
assignments to const lvalues. */
const int x = 1;
#ifdef T0
void f() {
x = 42;
......
/* run.config*
EXIT: 1
STDOPT:
*/
struct test{
int x;
int x;
......
/* run.config*
EXIT: 1
STDOPT:
*/
// Tests related to flexible array members
// FAM declaration OK
struct {
struct { // FAM declaration OK
int len;
char a[];
} fam;
// static FAM initialization not allowed (unsupported GCC extension)
struct {
struct {// static FAM initialization not allowed (unsupported GCC extension)
int len;
char a[];
} fam2 = {1, {1, 2, 3, 4, 5, 6}};
......
/* run.config
EXIT: 1
STDOPT:
*/
// invalid flexible array member (empty struct otherwise)
struct s1 {
char data[];
......
/* run.config*
EXIT: 1
STDOPT:
*/
// invalid flexible array member (two incomplete fields)
struct s {
int len;
......
/* run.config*
EXIT: 1
STDOPT:
*/
// invalid flexible array member (two incomplete fields in same field group)
struct s {
int len;
......
/* run.config*
EXIT: 1
STDOPT:
*/
// invalid flexible array member (incomplete field is not last)
struct s {
int len;
......
/* run.config*
EXIT: 1
STDOPT:
*/
// In C99, flexible array members cannot be nested inside other structs
typedef struct {
int a;
char data[];
......
/* run.config*
EXIT: 1
STDOPT:
*/
typedef int int_array [10] ;
struct Type { int field ; } ;
......@@ -187,4 +192,4 @@ void ghost_calls(void){
//@ ghost int g;
//@ ghost ghost_decl_nothing(&g);
//@ ghost ghost_def_nothing(&g);
}
\ No newline at end of file
}
/* run.config*
EXIT: 1
STDOPT:
*/
// In this file, each write raises an error: writing non-ghost memory location
// from ghost code, except if a comment says the opposite.
......@@ -157,4 +161,4 @@ void ghost_calls_to_non_ghost_functions(){
int x2 = int_assigns_nothing(&g);
int x3 = int_assigns_parameter(&g);
*/
}
\ No newline at end of file
}
/* run.config
EXIT: 1
OPT:-cpp-extra-args="-DIN_TYPE"
OPT:-cpp-extra-args="-DIN_DECL"
OPT:-cpp-extra-args="-DIN_GHOST_ATTR"
*/
// All of this should be refused
#ifdef IN_TYPE
struct S {
......
/* run.config
CMXS: @PTEST_NAME@
EXIT: 1
OPT:-cpp-extra-args="-DFAIL_DECL_TYPE"
EXIT: 0
OPT:-load-module %{dep:@PTEST_NAME@.cmxs}
*/
/* When there is no comment, the code should be allowed */
void f_ints(){
int ng ;
......
/* run.config
EXIT: 1
OPT: -no-autoload-plugins -cpp-extra-args="-DERROR_LOC_WITH_COMMENTS"
EXIT: 0
OPT: -no-autoload-plugins -cpp-extra-args="-DALREADY_HAS_ELSE" -print -kernel-warn-key ghost:bad-use=feedback
EXIT: 1
OPT: -no-autoload-plugins -cpp-extra-args="-DBAD_ANNOT_POSITION"
*/
#ifdef ERROR_LOC_WITH_COMMENTS // Must check that the line indicated for undeclared "z" is correct
void if_ghost_else_block_comments_then_error(int x, int y) {
if (x) {
x++;
......@@ -52,4 +52,4 @@ void test(int x, int y){
*/
}
#endif
\ No newline at end of file
#endif
/* run.config
OPT: -no-autoload-plugins -print
EXIT: 1
OPT: -print
*/
void if_ghost_else_one_line_bad(int x, int y) {
if (x) {
x++;
} //@ ghost else
y++;
}
\ No newline at end of file
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment