forked from awslabs/AutoCorrode
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathAutoCorrode.thy
More file actions
55 lines (53 loc) · 2.08 KB
/
AutoCorrode.thy
File metadata and controls
55 lines (53 loc) · 2.08 KB
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
(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
SPDX-License-Identifier: MIT *)
(*<*)
theory AutoCorrode
imports
"Autogen.Autogen"
"Byte_Level_Encoding.Byte_Level_Encoding"
"Crush.Crush"
"Data_Structures.Data_Structures"
"iq.iq"
"Micro_Rust_Examples.Micro_Rust_Examples"
"Micro_Rust_Interfaces.Micro_Rust_Interfaces"
"Micro_Rust_Interfaces_Core.Micro_Rust_Interfaces_Core"
"Micro_Rust_Parsing_Frontend.Micro_Rust_Parsing_Frontend"
"Micro_Rust_Runtime.Micro_Rust_Runtime"
"Micro_Rust_Std_Lib.Micro_Rust_Std_Lib"
"Micro_C_Parsing_Frontend.C_To_Core_Translation"
"Micro_C_Parsing_Frontend.C_File_Load_Smoke"
"Micro_C_Parsing_Frontend.C_Parser_Smoke"
"Micro_C_Parsing_Frontend.C_Translation_Smoke_Advanced"
"Micro_C_Parsing_Frontend.C_Translation_Smoke_Control"
"Micro_C_Parsing_Frontend.C_Translation_Smoke_Core"
"Micro_C_Parsing_Frontend.C_Translation_Smoke_Memory"
"Micro_C_Parsing_Frontend.C_Translation_Smoke_Options"
"Micro_C_Parsing_Frontend.C_Translation_Smoke_Types"
"Micro_C_Parsing_Frontend.C_Translation_Smoke_ILP32"
"Micro_C_Parsing_Frontend.C_Translation_Smoke_Compiler"
"Shallow_Micro_C.C_Arithmetic_Rules"
"Shallow_Micro_C.C_Abort"
"Shallow_Micro_C.C_Abort_Rules"
"Shallow_Micro_C.C_Byte_Encoding"
"Shallow_Micro_C.C_Void_Pointer"
"Shallow_Micro_C.C_Memory_Operations"
"Shallow_Micro_C.C_Numeric_Types"
"Shallow_Micro_C.C_Sizeof"
"Micro_C_Examples.C_ABI_Examples"
"Micro_C_Examples.Simple_C_Functions"
"Micro_C_Examples.C_Struct_Examples"
"Micro_C_Examples.C_Array_Examples"
"Micro_C_Examples.C_Bitwise_Examples"
"Micro_C_Examples.C_While_Examples"
"Micro_C_Examples.C_Void_Pointer_Examples"
"Micro_C_Examples.C_Union_Examples"
"Micro_C_Examples.C_Byte_Refinement"
"Micro_C_Examples.C_Misc_Examples"
"Misc.Misc"
"Lenses_And_Other_Optics.Lenses_And_Other_Optics"
"Separation_Lenses.Separation_Lenses"
"Shallow_Micro_Rust.Shallow_Micro_Rust"
"Shallow_Separation_Logic.Shallow_Separation_Logic"
begin
end
(*>*)