diff --git a/core/src/main/scala/stainless/genc/CAST.scala b/core/src/main/scala/stainless/genc/CAST.scala
index 7d325c9b5c..9d8e987aef 100644
--- a/core/src/main/scala/stainless/genc/CAST.scala
+++ b/core/src/main/scala/stainless/genc/CAST.scala
@@ -44,7 +44,7 @@ object CAST { // C Abstract Syntax Tree
   case class Prog(
     includes: Set[Include],
     // boolean is set to true when for global declarations that are declared outside of the Stainless program
-    decls: Seq[(Decl, Boolean)],
+    decls: Seq[(Decl, DeclarationMode)],
     typeDefs: Set[TypeDef],
     enums: Set[Enum],
     types: Seq[DataType], // Both structs and unions, order IS important! See NOTE above.
diff --git a/core/src/main/scala/stainless/genc/CPrinter.scala b/core/src/main/scala/stainless/genc/CPrinter.scala
index e2ea1c12c0..3e76b5893d 100644
--- a/core/src/main/scala/stainless/genc/CPrinter.scala
+++ b/core/src/main/scala/stainless/genc/CPrinter.scala
@@ -61,7 +61,11 @@ class CPrinter(
               sep = "\n\n")
              }
             |${nary(
-              decls.filter(!_._2).map(_._1),
+              decls.filter(_._2 != External).map {
+                case (decl, Static) => StaticStorage(decl)
+                case (decl, Normal) => decl
+                case _ => sys.error("unreachable code")
+              },
               opening = separator("global variables"),
               closing = ";\n\n",
               sep = ";\n")
@@ -269,8 +273,7 @@ class CPrinter(
   }
 
   private[genc] def pp(wt: WrapperTree)(implicit pctx: PrinterContext): Unit = wt match {
-    case StaticStorage(id) if id.name == "main" => /* Nothing */
-    case StaticStorage(_) => c"static "
+    case StaticStorage(decl) => c"static $decl"
 
     case TypeId(FunType(ret, params), id) => c"$ret (*$id)($params)"
     case TypeId(FixedArrayType(base, length), id) => c"$base $id[$length]"
@@ -316,7 +319,7 @@ class CPrinter(
 
   /** Wrappers to distinguish how the data should be printed **/
   private[genc] sealed abstract class WrapperTree
-  private case class StaticStorage(id: Id) extends WrapperTree
+  private case class StaticStorage(decl: Decl) extends WrapperTree
   private case class TypeId(typ: Type, id: Id) extends WrapperTree
   private case class FunSign(f: Fun) extends WrapperTree
 
diff --git a/core/src/main/scala/stainless/genc/GenCComponent.scala b/core/src/main/scala/stainless/genc/GenCComponent.scala
index 36b14bb16d..c8276e73d3 100644
--- a/core/src/main/scala/stainless/genc/GenCComponent.scala
+++ b/core/src/main/scala/stainless/genc/GenCComponent.scala
@@ -81,7 +81,7 @@ class GenCRun(override val pipeline: extraction.StainlessPipeline) // pipeline i
       override val results = ids.flatMap { id =>
         val fd = symbols.getFunction(id)
         val pos = fd.getPos.toString
-        if (fd.flags.exists(_.name == "export"))
+        if (fd.flags.exists(_.name == "cCode.export"))
           Some(GenCRun.Result(fd, Compiled, 0))
         else
           None
diff --git a/core/src/main/scala/stainless/genc/ir/IR.scala b/core/src/main/scala/stainless/genc/ir/IR.scala
index c3454d81da..86779db965 100644
--- a/core/src/main/scala/stainless/genc/ir/IR.scala
+++ b/core/src/main/scala/stainless/genc/ir/IR.scala
@@ -40,8 +40,7 @@ private[genc] sealed trait IR { ir =>
   sealed abstract class Def extends Tree
 
   case class Prog(
-    // boolean is set to true when for global declarations that are declared outside of the Stainless program
-    decls: Seq[(Decl, Boolean)],
+    decls: Seq[(Decl, DeclarationMode)],
     functions: Seq[FunDef],
     classes: Seq[ClassDef]
   ) {
diff --git a/core/src/main/scala/stainless/genc/ir/IRPrinter.scala b/core/src/main/scala/stainless/genc/ir/IRPrinter.scala
index b5d85cc40e..85fb555325 100644
--- a/core/src/main/scala/stainless/genc/ir/IRPrinter.scala
+++ b/core/src/main/scala/stainless/genc/ir/IRPrinter.scala
@@ -53,7 +53,7 @@ final class IRPrinter[S <: IR](val ir: S) {
     val post = ptx.newLine + "}"
 
     (if (fd.isPure) "@pure\n" else "") +
-    (if (fd.isExported) "@export\n" else "") +
+    (if (fd.isExported) "@cCode.export\n" else "") +
     pre + body + post
   }
 
diff --git a/core/src/main/scala/stainless/genc/package.scala b/core/src/main/scala/stainless/genc/package.scala
index 628367f569..dac375b978 100644
--- a/core/src/main/scala/stainless/genc/package.scala
+++ b/core/src/main/scala/stainless/genc/package.scala
@@ -21,4 +21,10 @@ package object genc {
 
   // FIXME: see leon definition
   def pathFromRoot(df: Definition)(implicit syms: Symbols): List[Definition] = List(df)
+
+  // declaration mode for global variables
+  sealed abstract class DeclarationMode
+  case object Normal extends DeclarationMode
+  case object Static extends DeclarationMode // static annotation
+  case object External extends DeclarationMode // no declaration in the produced code
 }
diff --git a/core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala b/core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala
index 602a4c160b..a2f833b194 100644
--- a/core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala
+++ b/core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala
@@ -16,8 +16,8 @@ import ExtraOps._
 import collection.mutable.{Set => MutableSet}
 
 /*
- * Compute the dependencies of the @export functions
- * Generic functions cannot be marked @export (only specialized versions that are
+ * Compute the dependencies of the @cCode.export functions
+ * Generic functions cannot be marked @cCode.export (only specialized versions that are
  * used by exported functions are exported to C).
  *
  * Moreover, the list of dependencies only contains top level functions. For nested
@@ -26,11 +26,6 @@ import collection.mutable.{Set => MutableSet}
  * some type T, then T (and all its class hierarchy if T is a class) will be included
  * in the dependency set.
  *
- * This phase also make sures @cCode.drop functions are not used. The same is *NOT*
- * done for dropped types as they might still be present in function signature. They
- * should be removed in a later (transformation) phase. Additionally, this phase
- * ensures that the annotation set on class and function is sane.
- *
  * NOTE We cannot rely on purescala.DependencyFinder as it will traverse functions
  *     annotated with @cCode.function and we don't want that. The same applies for
  *     classes annotated with @cCode.typdef. We therefore implement a simpler version
diff --git a/core/src/main/scala/stainless/genc/phases/ExtraOps.scala b/core/src/main/scala/stainless/genc/phases/ExtraOps.scala
index 19515b14e7..d9a98476ab 100644
--- a/core/src/main/scala/stainless/genc/phases/ExtraOps.scala
+++ b/core/src/main/scala/stainless/genc/phases/ExtraOps.scala
@@ -48,7 +48,7 @@ private[genc] object ExtraOps {
 
     def isExtern          = fd.flags contains Extern
     def isDropped         = hasAnnotation("cCode.drop") || fd.flags.contains(Ghost)
-    def isExported        = hasAnnotation("export")
+    def isExported        = hasAnnotation("cCode.export")
     def isManuallyDefined = hasAnnotation(manualDefAnnotation)
 
     def extAnnotations: Map[String, Seq[Any]] = fd.flags.collect {
@@ -77,7 +77,7 @@ private[genc] object ExtraOps {
   implicit class ClassDefOps(val cd: ClassDef) {
     def isManuallyTyped = hasAnnotation(manualTypeAnnotation)
     def isDropped       = hasAnnotation(droppedAnnotation)
-    def isExported      = hasAnnotation("export")
+    def isExported      = hasAnnotation("cCode.export")
     def isGlobal        = cd.flags.exists(_.name.startsWith("cCode.global"))
     def isGlobalDefault = cd.flags.exists(_.name == "cCode.global")
     def isGlobalUninitialized = cd.flags.exists(_.name == "cCode.globalUninitialized")
diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
index a54d670ede..ea48f8631d 100644
--- a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
+++ b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
@@ -107,7 +107,7 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
   def run(): Unit = {
     checkGlobalUsage()
 
-    // Start the transformation from `@exported` (and `@cCode.global`) functions and classes
+    // Start the transformation from `@cCode.export` (and `@cCode.global`) functions and classes
     for (df <- deps.deps) {
       df match {
         case fd: FunDef if fd.isExported =>
@@ -123,7 +123,7 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
    *                                                       Caches                                     *
    ****************************************************************************************************/
 
-  var declResults = new scala.collection.mutable.ListBuffer[(CIR.Decl, Boolean)]()
+  var declResults = new scala.collection.mutable.ListBuffer[(CIR.Decl, DeclarationMode)]()
 
   // For functions, we associate each TypedFunDef to a CIR.FunDef for each "type context" (TypeMapping).
   // This is very important for (non-generic) functions nested in a generic function because for N
@@ -643,18 +643,20 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
               s"We found ${paramInits.length} initializations instead of ${fields.length}."
             )
           }
-          for ((field, paramInit) <- fields.zip(paramInits)) {
+          for (((field, paramInit), static) <- fields.zip(paramInits).zip(nonGhostFields.map(vd => vd.flags.exists(_.name == "cCode.static")))) {
             implicit val emptyEnv = Env(Map(), Map(), false)
-            val decl = (CIR.Decl(field, Some(rec(paramInit.fullBody))), false)
+            val decl = (CIR.Decl(field, Some(rec(paramInit.fullBody))), if (static) Static else Normal)
             if (declResults.map(_._1.vd).contains(field)) {
               reporter.fatalError(cd.getPos, s"Global variable ${field.id} is defined twice")
             }
             declResults.append(decl)
           }
         } else if (cd.isGlobalUninitialized) {
-          for (field <- fields) declResults.append((CIR.Decl(field, None), false))
+          for ((field, static) <- fields.zip(nonGhostFields.map(vd => vd.flags.exists(_.name == "cCode.static")))) {
+            declResults.append((CIR.Decl(field, None), if (static) Static else Normal))
+          }
         } else if (cd.isGlobalExternal) {
-          for (field <- fields) declResults.append((CIR.Decl(field, None), true))
+          for (field <- fields) declResults.append((CIR.Decl(field, None), External))
         }
         newAcc
       } else {
diff --git a/core/src/sphinx/genc.rst b/core/src/sphinx/genc.rst
index d26a96ebec..66187d567a 100644
--- a/core/src/sphinx/genc.rst
+++ b/core/src/sphinx/genc.rst
@@ -135,7 +135,7 @@ See below for a case class with a fixed length array and its transformation in C
   val CONSTANT2: UInt16 = 12
   val CONSTANT3: UInt16 = CONSTANT1 + CONSTANT2
 
-  @export
+  @cCode.export
   case class W(x: Int, a: Array[Int], y: Int) {
     require(
       a.length == CONSTANT3.toInt &&
@@ -340,7 +340,7 @@ make sure that the instance is created using the default values:
 
 .. code-block:: scala
 
-  @export
+  @cCode.export
   def main() {
     implicit val gs = GlobalState()
     StdOut.print(gs.x)
diff --git a/frontends/benchmarks/genc/ArgumentsEffects.scala b/frontends/benchmarks/genc/ArgumentsEffects.scala
index 41c86d2662..ad81c44b36 100644
--- a/frontends/benchmarks/genc/ArgumentsEffects.scala
+++ b/frontends/benchmarks/genc/ArgumentsEffects.scala
@@ -12,7 +12,7 @@ object ArgumentsEffects {
     StdOut.println(x3)
   }
 
-  @export
+  @cCode.export
   def main(): Unit = {
     var x = 0
 
diff --git a/frontends/benchmarks/genc/FixedArray.scala b/frontends/benchmarks/genc/FixedArray.scala
index c96f317886..ae9323ec0e 100644
--- a/frontends/benchmarks/genc/FixedArray.scala
+++ b/frontends/benchmarks/genc/FixedArray.scala
@@ -8,7 +8,7 @@ object FixedArray {
   val CONSTANT2: UInt16 = 3
   val CONSTANT3: UInt16 = CONSTANT1 + CONSTANT2
 
-  @export
+  @cCode.export
   case class W(x: Int, a: Array[Int], y: Int) {
     require(
       a.length == CONSTANT3.toInt &&
@@ -17,7 +17,7 @@ object FixedArray {
     )
   }
 
-  @export
+  @cCode.export
   def f(w: W): Int = {
     require(0 <= w.a(0) && w.a(0) <= 1000)
     require(0 <= w.a(1) && w.a(1) <= 1000)
@@ -30,7 +30,7 @@ object FixedArray {
     w.a(0) + w.a(1) + w.a(2) + w.a(3) + w.a(4) + w.x + w.y
   }
 
-  @export
+  @cCode.export
   def g(a: Array[Int]): Unit = {
     require(a.length > 0)
     require(0 <= a(0) && a(0) <= 1000)
@@ -38,7 +38,7 @@ object FixedArray {
     a(0) += 1
   }
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val w = W(30, Array(10, 20, 30, 20, 42), 100)
     val w2 = W(30, Array(10, 20, 30, 20, 42), { w.a(0) += 1; 100 })
diff --git a/frontends/benchmarks/genc/Global.scala b/frontends/benchmarks/genc/Global.scala
index a4e8f32382..e032b8f386 100644
--- a/frontends/benchmarks/genc/Global.scala
+++ b/frontends/benchmarks/genc/Global.scala
@@ -31,7 +31,7 @@ object Global {
     if (state.y > 0) move()
   }.ensuring(_ => state.stable)
 
-  @export
+  @cCode.export
   def main() {
     implicit val gs = GlobalState()
     StdOut.print(gs.x)
diff --git a/frontends/benchmarks/genc/GlobalUninitialized.scala b/frontends/benchmarks/genc/GlobalUninitialized.scala
index 5bb52b52c0..de665e8f4c 100644
--- a/frontends/benchmarks/genc/GlobalUninitialized.scala
+++ b/frontends/benchmarks/genc/GlobalUninitialized.scala
@@ -31,7 +31,7 @@ object GlobalUninitialized {
     if (state.y > 0) move()
   }.ensuring(_ => state.stable)
 
-  @export
+  @cCode.export
   def main() {
     implicit val gs = GlobalState(Array.fill(100)(0), false, 0, 0)
     gs.x = 8
diff --git a/frontends/benchmarks/genc/ImageProcessing.scala b/frontends/benchmarks/genc/ImageProcessing.scala
index 0e076e4f6c..4bbea930dc 100644
--- a/frontends/benchmarks/genc/ImageProcessing.scala
+++ b/frontends/benchmarks/genc/ImageProcessing.scala
@@ -676,7 +676,7 @@ object ImageProcessing {
     else StdOut.println("false")
   }
 
-  @export
+  @cCode.export
   def main(): Int = {
     implicit val state = stainless.io.newState
     val input  = FIS.open("input.bmp")
diff --git a/frontends/benchmarks/genc/LZWa.scala b/frontends/benchmarks/genc/LZWa.scala
index b62ff78fb9..5f10776fa9 100644
--- a/frontends/benchmarks/genc/LZWa.scala
+++ b/frontends/benchmarks/genc/LZWa.scala
@@ -638,7 +638,7 @@ object LZWa {
     case _ => false
   }
 
-  @export
+  @cCode.export
   def main() = {
     implicit val state = stainless.io.newState
 
diff --git a/frontends/benchmarks/genc/LZWb.scala b/frontends/benchmarks/genc/LZWb.scala
index 74416b0107..bbcea1e346 100644
--- a/frontends/benchmarks/genc/LZWb.scala
+++ b/frontends/benchmarks/genc/LZWb.scala
@@ -715,7 +715,7 @@ object LZWb {
     case _ => false
   }
 
-  @export
+  @cCode.export
   def main() = {
     implicit val state = stainless.io.newState
 
diff --git a/frontends/benchmarks/genc/Nested.scala b/frontends/benchmarks/genc/Nested.scala
index 614c8a4606..a3b12f0e2a 100644
--- a/frontends/benchmarks/genc/Nested.scala
+++ b/frontends/benchmarks/genc/Nested.scala
@@ -4,7 +4,7 @@ import stainless.io._
 
 object Nested {
 
-  @export
+  @cCode.export
   def main(): Int = {
     f(100)
   }
diff --git a/frontends/benchmarks/genc/Normalisation.scala b/frontends/benchmarks/genc/Normalisation.scala
index 52597514a5..89682d16d3 100644
--- a/frontends/benchmarks/genc/Normalisation.scala
+++ b/frontends/benchmarks/genc/Normalisation.scala
@@ -14,7 +14,7 @@ object Normalisation {
   }
   case class B(a1: A, i: UInt8, j: UInt32, a2: A)
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val a = A(100, 9, 200)
     val x = a.sum + a.sum
diff --git a/frontends/benchmarks/genc/Pointer.scala b/frontends/benchmarks/genc/Pointer.scala
index 633b9dbea7..d7b2cfc1d6 100644
--- a/frontends/benchmarks/genc/Pointer.scala
+++ b/frontends/benchmarks/genc/Pointer.scala
@@ -10,7 +10,7 @@ object Pointer {
     r2.x = 250
   }
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val r = Pointer(100)
     val r2 = Pointer(100)
diff --git a/frontends/benchmarks/genc/Return.scala b/frontends/benchmarks/genc/Return.scala
index b308ece523..f6f268cec8 100644
--- a/frontends/benchmarks/genc/Return.scala
+++ b/frontends/benchmarks/genc/Return.scala
@@ -22,7 +22,7 @@ object Return {
     else StdOut.println("ERROR")
   }
 
-  @export
+  @cCode.export
   def main() = {
     verify(return10 == 10)
     verify(findIndex(Array(0,100,200,250), 0) == 0)
diff --git a/frontends/benchmarks/genc/StateTest.scala b/frontends/benchmarks/genc/StateTest.scala
index 05e1158249..b79e9df948 100644
--- a/frontends/benchmarks/genc/StateTest.scala
+++ b/frontends/benchmarks/genc/StateTest.scala
@@ -3,7 +3,7 @@ import stainless.lang._
 
 object StateTest {
 
-  @export
+  @cCode.export
   def main(): Int = {
     implicit val state = stainless.io.newState
     f()
diff --git a/frontends/benchmarks/genc/TwoOptions.scala b/frontends/benchmarks/genc/TwoOptions.scala
index 671c6e1e91..64b696ad3c 100644
--- a/frontends/benchmarks/genc/TwoOptions.scala
+++ b/frontends/benchmarks/genc/TwoOptions.scala
@@ -5,7 +5,7 @@ import stainless.annotation._
 
 object TwoOptions {
 
-  @export
+  @cCode.export
   def twoOptions: Unit = {
     var opt1: Option[Long] = None()
     val opt2: Option[Int] = None()
@@ -13,7 +13,7 @@ object TwoOptions {
     opt2.isEmpty
   }
 
-  @export
+  @cCode.export
   def main() = {
   }
 
diff --git a/frontends/benchmarks/genc/Unsigned.scala b/frontends/benchmarks/genc/Unsigned.scala
index 62ebd0313e..1550457605 100644
--- a/frontends/benchmarks/genc/Unsigned.scala
+++ b/frontends/benchmarks/genc/Unsigned.scala
@@ -5,7 +5,7 @@ import stainless.io._
 
 object Unsigned {
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val a = fa(16, 84)
     val b = fb(84, 14)
diff --git a/frontends/benchmarks/genc/WhileInLet.scala b/frontends/benchmarks/genc/WhileInLet.scala
index 47d2b54122..434b0c503c 100644
--- a/frontends/benchmarks/genc/WhileInLet.scala
+++ b/frontends/benchmarks/genc/WhileInLet.scala
@@ -2,7 +2,7 @@ import stainless.annotation._
 
 object WhileInLet {
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val noLoop = while (false) {}
     ()
diff --git a/frontends/benchmarks/imperative/valid/LetTargets.scala b/frontends/benchmarks/imperative/valid/LetTargets.scala
index f575d4851e..434f548f65 100644
--- a/frontends/benchmarks/imperative/valid/LetTargets.scala
+++ b/frontends/benchmarks/imperative/valid/LetTargets.scala
@@ -8,7 +8,7 @@ object LetTargets {
   case class C(bs: Array[B])
   case class D(val c: C)
 
-  @export
+  @cCode.export
   def reset(d: D): Unit = {
     require(d.c.bs.length > 0)
     require(d.c.bs(0).as.length > 0)
diff --git a/frontends/library/stainless/annotation/annotations.scala b/frontends/library/stainless/annotation/annotations.scala
index 52f42accac..c35847da81 100644
--- a/frontends/library/stainless/annotation/annotations.scala
+++ b/frontends/library/stainless/annotation/annotations.scala
@@ -95,10 +95,6 @@ class erasable extends Annotation
 @ignore
 class indexedAt(n: BigInt) extends Annotation
 
-/** Export function to C for GenC translation */
-@ignore
-class export extends Annotation
-
 @ignore
 class refEq extends Annotation
 
diff --git a/frontends/library/stainless/annotation/cCode.scala b/frontends/library/stainless/annotation/cCode.scala
index e4389a9e4a..8aba1f4ecc 100644
--- a/frontends/library/stainless/annotation/cCode.scala
+++ b/frontends/library/stainless/annotation/cCode.scala
@@ -2,7 +2,8 @@
 
 package stainless.annotation
 
-import scala.annotation.StaticAnnotation
+import scala.annotation.meta._
+import scala.annotation.{Annotation, StaticAnnotation}
 
 object cCode {
 
@@ -52,6 +53,10 @@ object cCode {
     includes: String
   ) extends StaticAnnotation
 
+  /* Export function into a header file for GenC translation */
+  @ignore
+  class export extends StaticAnnotation
+
   /*
    * Allows the user to define a type (e.g. case class) as a typeDef to an
    * existing type with an optional include file.
@@ -70,11 +75,8 @@ object cCode {
 
 
   /*
-   * Functions or types annotated with @cCode.drop will not be considered by
-   * GenC.
-   *
-   * It is therefore illegal to call such functions or use such types from
-   * within the code that is considered for C code conversion.
+   * Functions or types definitions annotated with @cCode.drop will not be translated by
+   * GenC. This implies the @extern annotation for verification in Stainless.
    */
   @ignore
   class drop() extends StaticAnnotation
@@ -97,4 +99,7 @@ object cCode {
   @ignore
   class globalExternal() extends StaticAnnotation
 
+  /* The `static` annotation can be used to mark variables that appear in `@global` annotated classes */
+  @ignore @field @getter @setter @param
+  class static() extends StaticAnnotation
 }
diff --git a/frontends/library/stainless/io/FileInputStream.scala b/frontends/library/stainless/io/FileInputStream.scala
index 2503f76520..cc613ca57c 100644
--- a/frontends/library/stainless/io/FileInputStream.scala
+++ b/frontends/library/stainless/io/FileInputStream.scala
@@ -92,7 +92,6 @@ case class FileInputStream(var filename: Option[String], var consumed: BigInt) {
 
   // Implementation detail
   @library
-  @extern
   @cCode.drop
   private def nativeReadByte(seed: BigInt): (Boolean, Byte) = {
     val in = new java.io.FileInputStream(filename.get)
diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala
index 5eb7622627..b8c577a38f 100644
--- a/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala
+++ b/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala
@@ -513,7 +513,7 @@ trait CodeExtraction extends ASTExtractors {
         (Seq(xt.IsInvariant) ++
           annots.filterNot(annot =>
             annot == xt.IsMutable ||
-            annot.name == "export" ||
+            annot.name == "cCode.export" ||
             annot.name.startsWith("cCode.global")
           )
         ).distinct
@@ -609,6 +609,10 @@ trait CodeExtraction extends ASTExtractors {
         Seq(xt.IsAccessor(Option(getIdentifier(sym.accessedOrSelf)).filterNot(_ => isAbstract)))
       else Seq())
 
+    // @cCode.drop implies @extern
+    if (flags.exists(_.name == "cCode.drop"))
+      flags :+= xt.Extern
+
     if (sym.name == nme.unapply) {
       def matchesParams(member: Symbol) = member.paramss match {
         case Nil        => true