Unexpected verification result related to some builtin functions

[muchang]

#include <assert.h>

const char *s1="-----BEGIN RSA PRIVATE KEY-----";

int main()
{

  if (strncmp(s1, "-----BEGIN ", 11))
    {assert(0);}

  return 0;
}

#include <assert.h>
char f(char a, char c)
{
  if (!a)
    { c = !c; } 
  return c;
}

void checkf(int a, int b)
{
  char c = f(a, b);
  char d;
  memcpy (&d, &c, 1);
  if ( (d != (a==0)) ^b)
    { assert(0); }
}

int main(void)
{
  checkf(0, 0);
  return 0;
}

CBMC version: 5.10
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc <file.c>
What behaviour did you expect:Result in SUCCESS (proofed by compiling with gcc and executing)
What happened instead:[foo.assertion.1] assertion 0: FAILURE

int main()
{
  char pattern[] = "a";
  int m = strlen (pattern);
  return 0;
}

void f(char *a)
{
  strcpy (a, "Hi!THE");
}


int main(void)
{
  char b[50] = {};
  f(b);
  return 0;
}

CBMC version: 5.10
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc <file.c>
What behaviour did you expect: Should terminate
What happened instead: Cannot Terminate

[tautschnig]

These tests pass as expected as of 10177c6 (#4673).