_CoqProject

-arg "-w -parsing"
-R . MicroPolicies

lib/utils.v
lib/haskell_notation.v
lib/ssr_list_utils.v
lib/ssr_set_utils.v
lib/fmap_utils.v
lib/word_utils.v

common/types.v
common/segment.v
common/printing.v

concrete/concrete.v
concrete/exec.v
concrete/int_32.v

symbolic/symbolic.v
symbolic/fault_handler.v
symbolic/refinement_common.v
symbolic/backward.v
symbolic/forward.v
symbolic/int_32.v
symbolic/rules.v
symbolic/exec.v

cfi/property.v
cfi/abstract.v
cfi/rules.v
cfi/symbolic.v
cfi/refinementAS.v
cfi/preservation.v
cfi/preservationAS.v
cfi/concrete.v
cfi/refinementSC.v
cfi/main.v
cfi/classes.v

memory_safety/classes.v
memory_safety/abstract.v
memory_safety/executable.v
memory_safety/symbolic.v
memory_safety/refinementAS.v
memory_safety/property.v
memory_safety/propertyA.v
memory_safety/propertyS.v
memory_safety/main.v

compartmentalization/ranges.v
compartmentalization/isolate_sets.v
compartmentalization/common.v
compartmentalization/abstract.v
compartmentalization/symbolic.v
compartmentalization/refinementSA.v
compartmentalization/main.v

sealing/classes.v
sealing/abstract.v
sealing/symbolic.v
sealing/refinementSA.v
sealing/main.v

ifc/symbolic.v
ifc/abstract.v
ifc/refinementSA.v
ifc/noninterference.v
ifc/noninterferenceS.v
ifc/labels.v
ifc/common.v

os/os.v

extraction/extraction.v