Ghost checker should disallow pattern matching on a ghost field

[romac]

import stainless.lang._
import stainless.annotation._

object GhostMatch {

  case class Foo(@ghost value: Option[BigInt])

  def nonGhostMatch(foo: Foo) = {
    foo match { // should fail because foo.value will not exist at runtime
      case Foo(Some(a)) => true
      case Foo(_) => false
    }
  }

  @ghost
  def ghostMatch(foo: Foo) = {
    foo match { // this is okay because we are in ghost context
      case Foo(Some(a)) => true
      case Foo(_) => false
    }
  }
}

[vkuncak]

Confirmed still reproducible on Version: 0.9.0-34-g88308df

[vkuncak]

This minor variant breaks --genc:

import stainless.lang._
import stainless.annotation._
object GhostMatch {
  case class Foo(@ghost value: Option[Int])
  def nonGhostMatch(foo: Foo): Int = {
    foo match { // should fail because foo.value will not exist at runtime
      case Foo(Some(a)) => 1
      case Foo(_) => 0
    }
  }
  @ghost
  def ghostMatch(foo: Foo) = {
    foo match { // this is okay because we are in ghost context
      case Foo(Some(a)) => true
      case Foo(_) => false
    }
  }
  @cCode.export
  def test(): Int = {
    nonGhostMatch(Foo(Some[Int](3)))
  }
  @extern
  def main(args: Array[String]): Unit = test  
}

[jad-hamza]

GenC itself doesn't do ghost checks (only ghost elimination). The checks are done by the GhostChecker I think even before the Stainless pipeline.