c-semantics/semantics/c/language/execution/configuration.k at master · kframework/c-semantics · GitHub

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
107
108
109
110
111
112
module C-CONFIGURATION
     imports BOOL-SYNTAX
     imports C-CONFIGURATION-EXTENSIONS
     imports C-EXECUTION-INIT-SYNTAX
     imports COMMON-CONFIGURATION
     imports COMMON-INIT-SYNTAX
     imports COMMON-SYNTAX
     imports DEFAULT-STRATEGY
     imports INT-SYNTAX
     imports LIBC-IO-SYNTAX
     imports LIST
     imports MAP
     imports SET
     imports SYMLOC-SYNTAX
     imports COMMON-THREAD-LOCAL

     syntax GeneratedTopCell

     configuration
<global />
<s />
<result-value color="red" exit=""> 139:EffectiveValue </result-value>
<T>
<exec multiplicity="?">
     <extensions-global/>

     <next-thread-id color="black"> 1 </next-thread-id>

     <compile-time-evaluation> true </compile-time-evaluation>

     <thread-info color="yellow">
          <thread-status color="yellow"> .Map </thread-status>
          <mutexes color="yellow"> .Map </mutexes>
          <glocks color="yellow"> .Map </glocks>
     </thread-info>
     <threads color="yellow" thread="">
          <thread multiplicity="*" color="yellow" type="Map">
               <thread-id color="yellow"> 0 </thread-id>

               <k color="green" multiplicity="?">
                    loadObj(unwrapObj($PGM:GeneratedTopCell))
                    ~> initMainThread(getEntryPoint($OPTIONS:Set))
                    ~> pgmArgs($ARGV:List)
                    ~> callEntryPoint(getEntryPoint($OPTIONS:Set), size($ARGV:List), incomingArguments($ARGV:List))
               </k>

               <final-computation multiplicity="?" color="lightgray">
                    .K
               </final-computation>
               <thread-local/>
          </thread>
     </threads>


</exec>

<error-cell multiplicity="?" color="black"> .K </error-cell>

<status> initializingTu </status>

<options> $OPTIONS:Set </options>

<library>
     // stdlib.h support
     <malloced color="lightgray"> .Map </malloced>
     // Stderr is unbuffered by default, but it can be changed.
     <atexit> flush(#stdout) ~> flush(#stderr) </atexit>
     <at-quick-exit> .K </at-quick-exit>

     // stdarg.h support.
     <va-lists> .Map </va-lists>
     // setjmp.h support.
     <jmp-bufs> .Map </jmp-bufs>

     <open-files> .Map </open-files>

     <files color="lightgray">
          <file multiplicity="*" type="Set">
               <fid> .K </fid>
               <uri> .K </uri>
               <pos> 0:IOInt </pos>
               <mode> "r" </mode>
               <next-byte> .K </next-byte>
               <read-buffer> "" </read-buffer>
               <write-buffer> "" </write-buffer>
               <buffer-mode> fullBuf </buffer-mode>
               <buffer-size> bufSiz </buffer-size>
               <sending> .List </sending>
               <done> "" </done>
               <feof> false </feof>
               <ferror> 0 </ferror>
               <last-op> noLastOp </last-op>
          </file>
     </files>
     <input color="lightgray"> .List </input>
     <output color="lightgray"> .List </output>
     // env key string |-> value ptr
     <strerror-cache> .Map </strerror-cache>
     <sig-handling-state> .K </sig-handling-state>
     // Cells to store pointers returned by these functions that are
     // invalidated by subsequent calls.
     <setlocale> NullPointerConstant </setlocale>
     <localeconv> NullPointerConstant </localeconv>
     <getenv> NullPointerConstant </getenv>
</library>


</T>

<json> $JSON:String </json>

endmodule