-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy path_CoqProject
106 lines (105 loc) · 3.09 KB
/
_CoqProject
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
-arg "-w all"
-arg "-w -disj-pattern-notation"
-arg "-w -notation-overridden"
-arg "-w -redundant-canonical-projection"
-Q case_study/MinimalCaps Katamaran.MinimalCaps
case_study/MinimalCaps/Base.v
case_study/MinimalCaps/Machine.v
case_study/MinimalCaps/Sig.v
case_study/MinimalCaps/Contracts/Notations.v
case_study/MinimalCaps/Contracts/Definitions.v
case_study/MinimalCaps/Contracts/Verification.v
case_study/MinimalCaps/Contracts/Statistics.v
case_study/MinimalCaps/Model.v
case_study/MinimalCaps/LoopVerification.v
-Q case_study/RiscvPmp Katamaran.RiscvPmp
case_study/RiscvPmp/Base.v
case_study/RiscvPmp/Machine.v
case_study/RiscvPmp/PmpCheck.v
case_study/RiscvPmp/Sig.v
case_study/RiscvPmp/Contracts.v
case_study/RiscvPmp/trace.v
case_study/RiscvPmp/IrisModel.v
case_study/RiscvPmp/IrisInstance.v
case_study/RiscvPmp/Model.v
case_study/RiscvPmp/IrisModelBinary.v
case_study/RiscvPmp/IrisInstanceBinary.v
case_study/RiscvPmp/ModelBinary.v
case_study/RiscvPmp/LoopVerification.v
case_study/RiscvPmp/LoopVerificationBinary.v
case_study/RiscvPmp/BlockVer/Examples.v
case_study/RiscvPmp/BlockVer/Spec.v
case_study/RiscvPmp/BlockVer/Verifier.v
case_study/RiscvPmp/FemtoKernel.v
case_study/Assumptions.v
-R theories Katamaran
test/Example.v
test/LinkedList.v
test/SumMaxLen.v
test/Replay.v
theories/Base.v
theories/BitvectorBase.v
theories/BitvectorSolve.v
theories/Bitvector.v
theories/Context.v
theories/Environment.v
theories/Iris/Instance.v
theories/Iris/Resources.v
theories/Iris/WeakestPre.v
theories/Iris/TotalWeakestPre.v
theories/Iris/Base.v
theories/Iris/BinaryResources.v
theories/Iris/BinaryWeakestPre.v
theories/Iris/BinaryAdequacy.v
theories/Iris/BinaryInstance.v
theories/Iris/cointro_patterns.v
theories/MicroSail/RefineExecutor.v
theories/MicroSail/ShallowExecutor.v
theories/MicroSail/ShallowSoundness.v
theories/MicroSail/Soundness.v
theories/MicroSail/SymbolicExecutor.v
theories/Notations.v
theories/Prelude.v
theories/Program.v
theories/Refinement/Monads.v
theories/Semantics.v
theories/Semantics/Registers.v
theories/Sep/Hoare.v
theories/Sep/Logic.v
theories/Shallow/Monads.v
theories/Signature.v
theories/SmallStep/Inversion.v
theories/SmallStep/Progress.v
theories/SmallStep/Step.v
theories/Specification.v
theories/Symbolic/Instantiation.v
theories/Symbolic/Monads.v
theories/Symbolic/OccursCheck.v
theories/Symbolic/PartialEvaluation.v
theories/Symbolic/Propositions.v
theories/Symbolic/Solver.v
theories/Symbolic/UnifLogic.v
theories/Symbolic/Worlds.v
theories/Syntax/Assertions.v
theories/Syntax/BinOps.v
theories/Syntax/Chunks.v
theories/Syntax/Expressions.v
theories/Syntax/Formulas.v
theories/Syntax/FunDecl.v
theories/Syntax/FunDef.v
theories/Syntax/Messages.v
theories/Syntax/Patterns.v
theories/Syntax/Predicates.v
theories/Syntax/Registers.v
theories/Syntax/Statements.v
theories/Syntax/Terms.v
theories/Syntax/TypeDecl.v
theories/Syntax/UnOps.v
theories/Syntax/Variables.v
theories/Tactics.v
theories/Staging/CommandStep.v
# theories/Staging/NewShallow/Executor.v
# theories/Staging/NewShallow/IrisInstance.v
# theories/Staging/NewShallow/Soundness.v
# theories/Staging/WorldInstance.v
# theories/Staging/WorldIsomorphisms.v