diff --git a/tests/cil/ghost_cfg.c b/tests/cil/ghost_cfg.c new file mode 100644 index 0000000000000000000000000000000000000000..a2faa9ed8c4f40fb1bdb95024bd94b3f39500da0 --- /dev/null +++ b/tests/cil/ghost_cfg.c @@ -0,0 +1,110 @@ +/* run.config + OPT:-no-autoload-plugins -cpp-extra-args="-DCAN_CHECK" + OPT:-no-autoload-plugins -cpp-extra-args="-DCANT_CHECK" +*/ + +#ifdef CAN_CHECK + +int first_stmt(void){ + //@ ghost goto X ; // breaks CFG by reaching "return 1" instead of "return 0" + return 0 ; + //@ ghost X: ; + return 1 ; +} + +void break_allowed(){ // OK + /*@ ghost + for(int i = 0 ; ; ++i){ + if(i == 10) break ; + } + */ +} + +void break_refuse(){ + int i = 0; + while(i < 10){ + //@ ghost if(i == 0) break ; // by-passes loop body + i++; + } +} + +void continue_refuse(){ + int i = 0; + while(i < 10){ + //@ ghost if(i == 0) continue ; // by-passes loop body + i++; + } +} + +void if_construct(int x){ // OK + //@ ghost int c ; + + x ++ ; + /*@ ghost + if (x == 0){ + c = 1 ; + } + else { + c = 2 ; + } + */ + x ++ ; +} + +void switch_construct(){ + int i = 42 ; + int x = 0 ; + //@ ghost int g ; + switch(i){ + case 0: x = 3 ; break ; + { /*@ ghost case 1: g = 3 ;*/ } // case 1 instead of going to default goes to case 2 + case 2: /*@ ghost g = 5 ;*/ i = 101 ; break ; + /*@ ghost case 3: g = 6 ; break ;*/ + } +} + +void block_with_assert(){ // OK + int x = 1 ; + + { + //@ assert x == 1 ; + } + + x = 2 ; +} + +int ghost_goto_non_ghost(){ + int x = 3 ; + + //@ ghost goto X ; // reaches return without executing "x = 2" + x = 2; + + X: + return 0; +} + +int ghost_goto_ghost(){ + int x = 3 ; + + //@ ghost goto X ; // reaches return without executing "x = 2" + x = 2; + + //@ ghost X: + return 0; +} + +#endif + +#ifdef CANT_CHECK + +int main(){ + goto X ; // This non-ghost goto cannot see the label "X" as it is ghost + + int x = 4 ; + + //@ ghost X: + + x = 2 ; +} + +#endif diff --git a/tests/cil/oracle/ghost_cfg.0.res.oracle b/tests/cil/oracle/ghost_cfg.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..894a8add56f382602ac67b182e5551de2f3899aa --- /dev/null +++ b/tests/cil/oracle/ghost_cfg.0.res.oracle @@ -0,0 +1,23 @@ +[kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing) +[kernel:ghost:bad-use] Warning: + Ghost code breaks CFG starting at: tests/cil/ghost_cfg.c:9 + /*@ ghost goto X; */ +[kernel:ghost:bad-use] Warning: + Ghost code breaks CFG starting at: tests/cil/ghost_cfg.c:26 + /*@ ghost if (i == 0) break; */ + i ++; +[kernel:ghost:bad-use] Warning: + Ghost code breaks CFG starting at: tests/cil/ghost_cfg.c:34 + /*@ ghost if (i == 0) continue; */ + i ++; +[kernel:ghost:bad-use] Warning: + Ghost code breaks CFG starting at: tests/cil/ghost_cfg.c:60 + case 1: /*@ ghost g = 3; */ +[kernel:ghost:bad-use] Warning: + Ghost code breaks CFG starting at: tests/cil/ghost_cfg.c:79 + /*@ ghost goto X; */ +[kernel:ghost:bad-use] Warning: + Ghost code breaks CFG starting at: tests/cil/ghost_cfg.c:89 + /*@ ghost goto X; */ +[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information. +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/cil/oracle/ghost_cfg.1.res.oracle b/tests/cil/oracle/ghost_cfg.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..c2186e30a0a76e5cff6886e386a55107d69bc1a3 --- /dev/null +++ b/tests/cil/oracle/ghost_cfg.1.res.oracle @@ -0,0 +1,6 @@ +[kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing) +[kernel:ghost:bad-non-ghost] Warning: + tests/cil/ghost_cfg.c:101: + 'goto X;' cannot see target label (ghost), removing ghost status of the label. +[kernel] Warning: warning ghost:bad-non-ghost treated as deferred error. See above messages for more information. +[kernel] Frama-C aborted: invalid user input.