val subroutine_stack_initializers:list initializer_t
val subroutine_stack_initializers:list initializer_t
let subroutine_stack_initializers: list initializer_t = 
  [

  ]
/// level A
/// {
///   ghost var a: int := 1;
///   ghost var c: int := 3;
///   ghost var e: int := 5;
/// 
///   method subroutine ()
///   {
///     a := 0;
///   }
/// 
///   method main ()
///   {
///     a := 10;
///     atomic {
///       c := 20;
///       e := 30;
///     }
///     subroutine();
///   }
/// }

module MyAProg

open Armada.Action
open Armada.Base
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Type
open Armada.Pointer
open Armada.Computation
open FStar.List.Tot
open FStar.Char
open FStar.Mul
open FStar.Sequence.Base
open Spec.Behavior
open Spec.Ubool

let global_initializers: list initializer_t =
  [
    { var_id = "a"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false; } ;
    { var_id = "c"; iv = InitializerSpecific (ObjectValueAbstract int 3); weakly_consistent = false; } ;
    { var_id = "e"; iv = InitializerSpecific (ObjectValueAbstract int 5); weakly_consistent = false; }
/
Spec.Ubool.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Char.fsti.checked Armada.Type.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyAProg.fst
Prims.list Armada.Init.initializer_t
Prims.Nil Armada.Init.initializer_t
let subroutine_stack_initializers:list initializer_t =
  
[]