pass.c

#include <assert.h>
#include <memory.h>
#include <klee/klee.h>


signed int sub_804858B(signed int a1, int a2)
{
  signed int result; // eax

  if ( a1 == a2 )
    result = a1;
  else
    result = 1;
  return result;
}

//----- (080485A2) --------------------------------------------------------
int sub_80485A2(signed int a1)
{
  signed int v1; // ebx

  v1 = sub_804858B(18, 18);
  return 5 * (v1 + sub_804858B(a1, 400));
}

//----- (080485EA) --------------------------------------------------------
int sub_80485EA(char* a1)
{
  int i = 0;
  for (i = 0; a1[i] && a1[i] != 10; ++i )
    ;
  return i;
}

//----- (08048623) --------------------------------------------------------
signed int sub_8048623(signed int a1)
{
  signed int i; // [esp+Ch] [ebp-4h]

  for ( i = sub_804858B(36, 36); sub_804858B(1, 1) != i; --i )
    a1 -= sub_804858B(a1, 1094861568);
  return a1;
}

//----- (08048668) --------------------------------------------------------
int sub_8048668(char* a1)
{

  int v1 = sub_80485EA(a1);
  return !sub_804858B(v1, 16)
      || *(char *)(sub_80485EA(a1) / 2 + 3 + a1) != 33
      || *(char *)(sub_80485EA(a1) / 2 + 4 + a1) != 33;
}

//----- (080486DF) --------------------------------------------------------
int sub_80486DF(char *a1)
{
  return a1[3] == 115 && a1[4] == 111 && a1[5] == 109;
}

//----- (08048717) --------------------------------------------------------
int sub_8048717(char *a1)
{
  return a1[13] == 59 && a1[14] == 45 && a1[15] == 41;
}

//----- (0804874F) --------------------------------------------------------
int sub_804874F(char *a1)
{
  return a1[8] != 77 || a1[9] != 48 || a1[10] != 118;
}

//----- (08048787) --------------------------------------------------------
int sub_8048787(char *a1)
{
  int v1; // ST14_4

  v1 = a1[2] - *a1 + 83;
  return a1[sub_804858B(*a1, a1[4])] == v1;
}

//----- (080487EB) --------------------------------------------------------
int main()
{
  int v0; // ebx
  char v1; // bl
  int v2; // ebx
  signed int v4; // [esp+0h] [ebp-10h]

  v4 = 16;
  char s[17] = "Awesome_M0v!!;-)";
  klee_make_symbolic(s, sizeof(s), "s");
  if ( sub_804858B(v4, 16) == v4 && sub_80485EA(s) == v4 )
  {
    v0 = s[v4 / 2 - 1];
    if ( v0 == sub_80485A2(v4) && s[sub_804858B(3, 3) - 1] == 101 )
    {
      v1 = s[6];
      if ( v1 == s[sub_804858B(2, 2)] )
      {
        v2 = *s;
        if ( v2 == sub_8048623(s[6]) - 1 )
        {
          if ( !sub_8048668(s) )
          {
            if ( sub_80486DF(s) )
            {
              if ( sub_8048717(s) )
              {
                if ( !sub_804874F(s) )
                {
                  if ( sub_8048787(s) )
                  {
                    klee_assert(0);
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  return 0;
}