Showing error 2320

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/toy_safe.cil.c
Line in file: 12
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

  1extern int __VERIFIER_nondet_int();
  2/* Generated by CIL v. 1.3.6 */
  3/* print_CIL_Input is true */
  4
  5
  6
  7void error(void) 
  8{ 
  9
 10  {
 11  goto ERROR;
 12  ERROR: ;
 13  return;
 14}
 15}
 16
 17int c  ;
 18int c_t  ;
 19int c_req_up  ;
 20int p_in  ;
 21int p_out  ;
 22int wl_st  ;
Show full sources