possible design pattern for using C enums #3750

typedef enum { RED, BLUE } Color;

Color nondet_color()
{
  int color = nondet_int();
  color = color < 0 ? -color : color;
  color = color % 2;
  return color;
}  

int is_color( Color color )
{
  return 0 <= color && color < 2;
}  

int main()
{
  Color qa;
  Color qb;

  //--------------------------------------------------
  // GOOD
  
  qa = nondet_color();
  qb = (qa == RED) ? BLUE : RED;

  __ESBMC_loop_invariant(
    is_color( qa ) &&
    is_color( qb ) &&
    (qa != qb)
  );
  for (int count = 0; count < 10; count++)
  {
    if (qa != RED && qb != RED)
    {
      qb = RED;
      qa = RED;
    }
    
  }

  //--------------------------------------------------
  // BAD
  
  qa = nondet_color();
  qb = (qa == RED) ? BLUE : RED;
  
  // This invariant fails in the inductive step,
  // because the invariant must include
  // is_color(qa) && is_color(qb)
  // is_color() is needed because the underlying implementation
  // of enums in C is int.
  __ESBMC_loop_invariant( qa != qb );
  for (int count = 0; count < 10; count++)
  {
    if (qa != RED && qb != RED)
    {
      qb = RED;
      qa = RED;
    }
  }
  
}