#include <divine.h>
#include <dios.h>

int main()
{
    int res, readsz;
    const char message[] = "hello world!\n";
    char buffer[32];

    __vm_syscall( 0 /* SYS_read */,
                  _VM_SC_Out | _VM_SC_Int32, &readsz, /* return value */
                  _VM_SC_In | _VM_SC_Int32, 0,        /* fd */
                  _VM_SC_Out | _VM_SC_Mem, sizeof( buffer ), buffer ,
                  _VM_SC_In | _VM_SC_Int64, sizeof( buffer ) );

    if ( !readsz )
        return 1;

    __vm_syscall( 1 /* SYS_write */,
                  _VM_SC_Out | _VM_SC_Int32, &res,
                  _VM_SC_In | _VM_SC_Int32, 1,
                  _VM_SC_In | _VM_SC_Mem, sizeof( message ), message,
                  _VM_SC_In | _VM_SC_Int64, sizeof( message ) );

    __vm_syscall( 1 /* SYS_write */,
                  _VM_SC_Out | _VM_SC_Int32, &res,
                  _VM_SC_In | _VM_SC_Int32, 1,
                  _VM_SC_In | _VM_SC_Mem, (long) readsz, buffer,
                  _VM_SC_In | _VM_SC_Int64, (long) readsz );

    __vm_syscall( 1 /* SYS_write */,
                  _VM_SC_Out | _VM_SC_Int32, &res,
                  _VM_SC_In | _VM_SC_Int32, 1,
                  _VM_SC_In | _VM_SC_Mem, 2lu, "\n" ,
                  _VM_SC_In | _VM_SC_Int64, 2lu );
}