open Preamble

open UtilBranch

open ASMCostsSplit

open StructuredTraces

open AbstractStatus

open StatusProofs

open Interpret

open ASMCosts

open Status

open Fetch

open Assembly

open PolicyFront

open PolicyStep

open Policy

open AssocList

open Uses

open ASM

open BitVectorTrieSet

open LINToASM

open LIN

open Linearise

open LTLToLIN

open Fixpoints

open Set_adt

open Liveness

open Interference

open Joint_LTL_LIN

open LTL

open ERTLToLTL

open ERTL

open RegisterSet

open RTLToERTL

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open String

open LabelledObjects

open I8051

open BackEndOps

open Joint

open RTL

open RTLabsToRTL

open CostInj

open Deqsets_extra

open CostMisc

open Listb_extra

open CostSpec

open CostCheck

open BitVectorTrie

open Graphs

open Order

open Registers

open RTLabs_syntax

open ToRTLabs

open FrontEndOps

open Cminor_syntax

open ToCminor

open MemProperties

open MemoryInjections

open Fresh

open SwitchRemoval

open Sets

open Listb

open Star

open Frontend_misc

open CexecInd

open Casts

open ClassifyOp

open Smallstep

open Extra_bool

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Globalenvs

open Csem

open SmallstepExec

open Division

open Z

open BitVectorZ

open Pointers

open Values

open Events

open IOMonad

open IO

open Cexec

open TypeComparison

open SimplifyCasts

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Csyntax

open Label

open Compiler

open Stacksize

open Executions

open Measurable

open Clight_abstract

open Clight_classified_system

open Cminor_semantics

open Cminor_abstract

open Cminor_classified_system

open RTLabs_semantics

open RTLabs_abstract

open RTLabs_classified_system

open ExtraMonads

open ExtraGlobalenvs

open I8051bis

open BEMem

open Joint_semantics

open SemanticsUtils

open Traces

open Joint_fullexec

open RTL_semantics

open ERTL_semantics

open Joint_LTL_LIN_semantics

open LTL_semantics

open LIN_semantics

open Interpret2

type preclassified_system_pass =
  Measurable.preclassified_system
  (* singleton inductive, whose constructor was mk_preclassified_system_pass *)

val preclassified_system_pass_rect_Type4 :
  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
  preclassified_system_pass -> 'a1

val preclassified_system_pass_rect_Type5 :
  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
  preclassified_system_pass -> 'a1

val preclassified_system_pass_rect_Type3 :
  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
  preclassified_system_pass -> 'a1

val preclassified_system_pass_rect_Type2 :
  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
  preclassified_system_pass -> 'a1

val preclassified_system_pass_rect_Type1 :
  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
  preclassified_system_pass -> 'a1

val preclassified_system_pass_rect_Type0 :
  Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
  preclassified_system_pass -> 'a1

val pcs_pcs :
  Compiler.pass -> preclassified_system_pass ->
  Measurable.preclassified_system

val preclassified_system_pass_inv_rect_Type4 :
  Compiler.pass -> preclassified_system_pass ->
  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1

val preclassified_system_pass_inv_rect_Type3 :
  Compiler.pass -> preclassified_system_pass ->
  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1

val preclassified_system_pass_inv_rect_Type2 :
  Compiler.pass -> preclassified_system_pass ->
  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1

val preclassified_system_pass_inv_rect_Type1 :
  Compiler.pass -> preclassified_system_pass ->
  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1

val preclassified_system_pass_inv_rect_Type0 :
  Compiler.pass -> preclassified_system_pass ->
  (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1

val pcs_pcs__o__pcs_exec :
  Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
  SmallstepExec.fullexec

val pcs_pcs__o__pcs_exec__o__es1 :
  Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
  SmallstepExec.trans_system

val preclassified_system_of_pass :
  Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass

val run_and_print :
  Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
  Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
  (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
  Types.unit0