CBMC
java.io.c File Reference

Go to the source code of this file.

Functions

 __CPROVER_assume (read_result >=-1 &&read_result<=255)
 

Variables

int __CPROVER_ID java::java io InputStream read
 
return read_result
 

Function Documentation

◆ __CPROVER_assume()

__CPROVER_assume ( read_result >=-1 &&read_result<=  255)

Variable Documentation

◆ read

ssize_t read

Definition at line 3 of file java.io.c.

◆ read_result

return read_result

Definition at line 7 of file java.io.c.