@@ -48,39 +48,44 @@ exe_sym_env_t __exe_env = {
4848};
4949
5050static void __create_new_dfile (exe_disk_file_t * dfile , unsigned size ,
51- const char * name , struct stat64 * defaults ) {
51+ const char * name , struct stat64 * defaults , unsigned standart_io ) {
5252 struct stat64 * s = malloc (sizeof (* s ));
5353 if (!s )
5454 klee_report_error (__FILE__ , __LINE__ , "out of memory in klee_init_env" , "user.err" );
5555
5656 const char * sp ;
5757 char sname [64 ];
58- char read_bytes_name [64 ];
59- char write_bytes_name [64 ];
6058 for (sp = name ; * sp ; ++ sp ){
6159 sname [sp - name ] = * sp ;
62- read_bytes_name [sp - name ] = * sp ;
63- write_bytes_name [sp - name ] = * sp ;
6460 }
6561 memcpy (& sname [sp - name ], "-stat" , 6 );
66- memcpy (& read_bytes_name [sp - name ], "-read" , 6 );
67- memcpy (& write_bytes_name [sp - name ], "-write" , 7 );
6862
6963 assert (size );
7064
7165 dfile -> size = size ;
7266 dfile -> contents = malloc (dfile -> size );
7367
74- unsigned * ptr_read = malloc (sizeof (unsigned ));
75- unsigned * ptr_write = malloc (sizeof (unsigned ));
76- klee_make_symbolic (ptr_read , sizeof (unsigned ), read_bytes_name );
77- klee_make_symbolic (ptr_write , sizeof (unsigned ), write_bytes_name );
78- memcpy (& dfile -> read_bytes_symbolic , ptr_read , sizeof (unsigned ));
79- memcpy (& dfile -> write_bytes_symbolic , ptr_write , sizeof (unsigned ));
80- free (ptr_read );
81- free (ptr_write );
82- dfile -> read_bytes_real = 0 ;
83- dfile -> write_bytes_real = 0 ;
68+ if (!standart_io ) {
69+ char read_bytes_name [64 ];
70+ char write_bytes_name [64 ];
71+ for (const char * sp = name ; * sp ; ++ sp ) {
72+ read_bytes_name [sp - name ] = * sp ;
73+ write_bytes_name [sp - name ] = * sp ;
74+ }
75+ memcpy (& read_bytes_name [sp - name ], "-read" , 6 );
76+ memcpy (& write_bytes_name [sp - name ], "-write" , 7 );
77+
78+ unsigned * ptr_read = malloc (sizeof (unsigned ));
79+ unsigned * ptr_write = malloc (sizeof (unsigned ));
80+ klee_make_symbolic (ptr_read , sizeof (unsigned ), read_bytes_name );
81+ klee_make_symbolic (ptr_write , sizeof (unsigned ), write_bytes_name );
82+ memcpy (& dfile -> read_bytes_symbolic , ptr_read , sizeof (unsigned ));
83+ memcpy (& dfile -> write_bytes_symbolic , ptr_write , sizeof (unsigned ));
84+ free (ptr_read );
85+ free (ptr_write );
86+ dfile -> read_bytes_real = 0 ;
87+ dfile -> write_bytes_real = 0 ;
88+ }
8489
8590 if (!dfile -> contents )
8691 klee_report_error (__FILE__ , __LINE__ , "out of memory in klee_init_env" , "user.err" );
@@ -151,15 +156,15 @@ void klee_init_fds(unsigned n_files, unsigned file_length,
151156
152157 for (k = 0 ; k < n_files ; k ++ ) {
153158 name [0 ] = 'A' + k ;
154- __create_new_dfile (& __exe_fs .sym_files [k ], file_length , name , & s );
159+ __create_new_dfile (& __exe_fs .sym_files [k ], file_length , name , & s , 0 );
155160 }
156161
157162 /* setting symbolic stdin */
158163 if (stdin_length ) {
159164 __exe_fs .sym_stdin = malloc (sizeof (* __exe_fs .sym_stdin ));
160165 if (!__exe_fs .sym_stdin )
161166 klee_report_error (__FILE__ , __LINE__ , "out of memory in klee_init_env" , "user.err" );
162- __create_new_dfile (__exe_fs .sym_stdin , stdin_length , "stdin" , & s );
167+ __create_new_dfile (__exe_fs .sym_stdin , stdin_length , "stdin" , & s , 1 );
163168 unsigned int i ;
164169 for (i = 0 ; i < stdin_length ; i ++ ) {
165170 klee_prefer_cex (__exe_fs .sym_stdin , 32 <= __exe_fs .sym_stdin -> contents [i ] & __exe_fs .sym_stdin -> contents [i ] <= 126 );
@@ -196,7 +201,7 @@ void klee_init_fds(unsigned n_files, unsigned file_length,
196201 __exe_fs .sym_stdout = malloc (sizeof (* __exe_fs .sym_stdout ));
197202 if (!__exe_fs .sym_stdout )
198203 klee_report_error (__FILE__ , __LINE__ , "out of memory in klee_init_env" , "user.err" );
199- __create_new_dfile (__exe_fs .sym_stdout , 1024 , "stdout" , & s );
204+ __create_new_dfile (__exe_fs .sym_stdout , 1024 , "stdout" , & s , 1 );
200205 __exe_env .fds [1 ].dfile = __exe_fs .sym_stdout ;
201206 __exe_fs .stdout_writes = 0 ;
202207 }
0 commit comments