1extern int __VERIFIER_nondet_int(void);
2
3
4
5#line 2 "libacc.c"
6struct JoinPoint {
7 void **(*fp)(struct JoinPoint * ) ;
8 void **args ;
9 int argsCount ;
10 char const **argsType ;
11 void *(*arg)(int , struct JoinPoint * ) ;
12 char const *(*argType)(int , struct JoinPoint * ) ;
13 void **retValue ;
14 char const *retType ;
15 char const *funcName ;
16 char const *targetName ;
17 char const *fileName ;
18 char const *kind ;
19 void *excep_return ;
20};
21#line 18 "libacc.c"
22struct __UTAC__CFLOW_FUNC {
23 int (*func)(int , int ) ;
24 int val ;
25 struct __UTAC__CFLOW_FUNC *next ;
26};
27#line 18 "libacc.c"
28struct __UTAC__EXCEPTION {
29 void *jumpbuf ;
30 unsigned long long prtValue ;
31 int pops ;
32 struct __UTAC__CFLOW_FUNC *cflowfuncs ;
33};
34#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
35typedef unsigned long size_t;
36#line 76 "libacc.c"
37struct __ACC__ERR {
38 void *v ;
39 struct __ACC__ERR *next ;
40};
41#line 1 "ClientLib.o"
42#pragma merger(0,"ClientLib.i","")
43#line 4 "ClientLib.h"
44int initClient(void) ;
45#line 6
46char *getClientName(int handle ) ;
47#line 8
48void setClientName(int handle , char *value ) ;
49#line 10
50int getClientOutbuffer(int handle ) ;
51#line 12
52void setClientOutbuffer(int handle , int value ) ;
53#line 14
54int getClientAddressBookSize(int handle ) ;
55#line 16
56void setClientAddressBookSize(int handle , int value ) ;
57#line 18
58int createClientAddressBookEntry(int handle ) ;
59#line 20
60int getClientAddressBookAlias(int handle , int index ) ;
61#line 22
62void setClientAddressBookAlias(int handle , int index , int value ) ;
63#line 24
64int getClientAddressBookAddress(int handle , int index ) ;
65#line 26
66void setClientAddressBookAddress(int handle , int index , int value ) ;
67#line 29
68int getClientAutoResponse(int handle ) ;
69#line 31
70void setClientAutoResponse(int handle , int value ) ;
71#line 33
72int getClientPrivateKey(int handle ) ;
73#line 35
74void setClientPrivateKey(int handle , int value ) ;
75#line 37
76int getClientKeyringSize(int handle ) ;
77#line 39
78int createClientKeyringEntry(int handle ) ;
79#line 41
80int getClientKeyringUser(int handle , int index ) ;
81#line 43
82void setClientKeyringUser(int handle , int index , int value ) ;
83#line 45
84int getClientKeyringPublicKey(int handle , int index ) ;
85#line 47
86void setClientKeyringPublicKey(int handle , int index , int value ) ;
87#line 49
88int getClientForwardReceiver(int handle ) ;
89#line 51
90void setClientForwardReceiver(int handle , int value ) ;
91#line 53
92int getClientId(int handle ) ;
93#line 55
94void setClientId(int handle , int value ) ;
95#line 57
96int findPublicKey(int handle , int userid ) ;
97#line 59
98int findClientAddressBookAlias(int handle , int userid ) ;
99#line 5 "ClientLib.c"
100int __ste_Client_counter = 0;
101#line 7 "ClientLib.c"
102int initClient(void)
103{ int retValue_acc ;
104
105 {
106#line 12 "ClientLib.c"
107 if (__ste_Client_counter < 3) {
108#line 684
109 __ste_Client_counter = __ste_Client_counter + 1;
110#line 684
111 retValue_acc = __ste_Client_counter;
112#line 686
113 return (retValue_acc);
114 } else {
115#line 692 "ClientLib.c"
116 retValue_acc = -1;
117#line 694
118 return (retValue_acc);
119 }
120#line 701 "ClientLib.c"
121 return (retValue_acc);
122}
123}
124#line 15 "ClientLib.c"
125char *__ste_client_name0 = (char *)0;
126#line 17 "ClientLib.c"
127char *__ste_client_name1 = (char *)0;
128#line 19 "ClientLib.c"
129char *__ste_client_name2 = (char *)0;
130#line 22 "ClientLib.c"
131char *getClientName(int handle )
132{ char *retValue_acc ;
133 void *__cil_tmp3 ;
134
135 {
136#line 31 "ClientLib.c"
137 if (handle == 1) {
138#line 732
139 retValue_acc = __ste_client_name0;
140#line 734
141 return (retValue_acc);
142 } else {
143#line 736
144 if (handle == 2) {
145#line 741
146 retValue_acc = __ste_client_name1;
147#line 743
148 return (retValue_acc);
149 } else {
150#line 745
151 if (handle == 3) {
152#line 750
153 retValue_acc = __ste_client_name2;
154#line 752
155 return (retValue_acc);
156 } else {
157#line 758 "ClientLib.c"
158 __cil_tmp3 = (void *)0;
159#line 758
160 retValue_acc = (char *)__cil_tmp3;
161#line 760
162 return (retValue_acc);
163 }
164 }
165 }
166#line 767 "ClientLib.c"
167 return (retValue_acc);
168}
169}
170#line 34 "ClientLib.c"
171void setClientName(int handle , char *value )
172{
173
174 {
175#line 42
176 if (handle == 1) {
177#line 36
178 __ste_client_name0 = value;
179 } else {
180#line 37
181 if (handle == 2) {
182#line 38
183 __ste_client_name1 = value;
184 } else {
185#line 39
186 if (handle == 3) {
187#line 40
188 __ste_client_name2 = value;
189 } else {
190
191 }
192 }
193 }
194#line 802 "ClientLib.c"
195 return;
196}
197}
198#line 44 "ClientLib.c"
199int __ste_client_outbuffer0 = 0;
200#line 46 "ClientLib.c"
201int __ste_client_outbuffer1 = 0;
202#line 48 "ClientLib.c"
203int __ste_client_outbuffer2 = 0;
204#line 50 "ClientLib.c"
205int __ste_client_outbuffer3 = 0;
206#line 53 "ClientLib.c"
207int getClientOutbuffer(int handle )
208{ int retValue_acc ;
209
210 {
211#line 62 "ClientLib.c"
212 if (handle == 1) {
213#line 831
214 retValue_acc = __ste_client_outbuffer0;
215#line 833
216 return (retValue_acc);
217 } else {
218#line 835
219 if (handle == 2) {
220#line 840
221 retValue_acc = __ste_client_outbuffer1;
222#line 842
223 return (retValue_acc);
224 } else {
225#line 844
226 if (handle == 3) {
227#line 849
228 retValue_acc = __ste_client_outbuffer2;
229#line 851
230 return (retValue_acc);
231 } else {
232#line 857 "ClientLib.c"
233 retValue_acc = 0;
234#line 859
235 return (retValue_acc);
236 }
237 }
238 }
239#line 866 "ClientLib.c"
240 return (retValue_acc);
241}
242}
243#line 65 "ClientLib.c"
244void setClientOutbuffer(int handle , int value )
245{
246
247 {
248#line 73
249 if (handle == 1) {
250#line 67
251 __ste_client_outbuffer0 = value;
252 } else {
253#line 68
254 if (handle == 2) {
255#line 69
256 __ste_client_outbuffer1 = value;
257 } else {
258#line 70
259 if (handle == 3) {
260#line 71
261 __ste_client_outbuffer2 = value;
262 } else {
263
264 }
265 }
266 }
267#line 901 "ClientLib.c"
268 return;
269}
270}
271#line 77 "ClientLib.c"
272int __ste_ClientAddressBook_size0 = 0;
273#line 79 "ClientLib.c"
274int __ste_ClientAddressBook_size1 = 0;
275#line 81 "ClientLib.c"
276int __ste_ClientAddressBook_size2 = 0;
277#line 84 "ClientLib.c"
278int getClientAddressBookSize(int handle )
279{ int retValue_acc ;
280
281 {
282#line 93 "ClientLib.c"
283 if (handle == 1) {
284#line 928
285 retValue_acc = __ste_ClientAddressBook_size0;
286#line 930
287 return (retValue_acc);
288 } else {
289#line 932
290 if (handle == 2) {
291#line 937
292 retValue_acc = __ste_ClientAddressBook_size1;
293#line 939
294 return (retValue_acc);
295 } else {
296#line 941
297 if (handle == 3) {
298#line 946
299 retValue_acc = __ste_ClientAddressBook_size2;
300#line 948
301 return (retValue_acc);
302 } else {
303#line 954 "ClientLib.c"
304 retValue_acc = 0;
305#line 956
306 return (retValue_acc);
307 }
308 }
309 }
310#line 963 "ClientLib.c"
311 return (retValue_acc);
312}
313}
314#line 96 "ClientLib.c"
315void setClientAddressBookSize(int handle , int value )
316{
317
318 {
319#line 104
320 if (handle == 1) {
321#line 98
322 __ste_ClientAddressBook_size0 = value;
323 } else {
324#line 99
325 if (handle == 2) {
326#line 100
327 __ste_ClientAddressBook_size1 = value;
328 } else {
329#line 101
330 if (handle == 3) {
331#line 102
332 __ste_ClientAddressBook_size2 = value;
333 } else {
334
335 }
336 }
337 }
338#line 998 "ClientLib.c"
339 return;
340}
341}
342#line 106 "ClientLib.c"
343int createClientAddressBookEntry(int handle )
344{ int retValue_acc ;
345 int size ;
346 int tmp ;
347 int __cil_tmp5 ;
348
349 {
350 {
351#line 107
352 tmp = getClientAddressBookSize(handle);
353#line 107
354 size = tmp;
355 }
356#line 108 "ClientLib.c"
357 if (size < 3) {
358 {
359#line 109 "ClientLib.c"
360 __cil_tmp5 = size + 1;
361#line 109
362 setClientAddressBookSize(handle, __cil_tmp5);
363#line 1025 "ClientLib.c"
364 retValue_acc = size + 1;
365 }
366#line 1027
367 return (retValue_acc);
368 } else {
369#line 1031 "ClientLib.c"
370 retValue_acc = -1;
371#line 1033
372 return (retValue_acc);
373 }
374#line 1040 "ClientLib.c"
375 return (retValue_acc);
376}
377}
378#line 115 "ClientLib.c"
379int __ste_Client_AddressBook0_Alias0 = 0;
380#line 117 "ClientLib.c"
381int __ste_Client_AddressBook0_Alias1 = 0;
382#line 119 "ClientLib.c"
383int __ste_Client_AddressBook0_Alias2 = 0;
384#line 121 "ClientLib.c"
385int __ste_Client_AddressBook1_Alias0 = 0;
386#line 123 "ClientLib.c"
387int __ste_Client_AddressBook1_Alias1 = 0;
388#line 125 "ClientLib.c"
389int __ste_Client_AddressBook1_Alias2 = 0;
390#line 127 "ClientLib.c"
391int __ste_Client_AddressBook2_Alias0 = 0;
392#line 129 "ClientLib.c"
393int __ste_Client_AddressBook2_Alias1 = 0;
394#line 131 "ClientLib.c"
395int __ste_Client_AddressBook2_Alias2 = 0;
396#line 134 "ClientLib.c"
397int getClientAddressBookAlias(int handle , int index )
398{ int retValue_acc ;
399
400 {
401#line 167
402 if (handle == 1) {
403#line 144 "ClientLib.c"
404 if (index == 0) {
405#line 1086
406 retValue_acc = __ste_Client_AddressBook0_Alias0;
407#line 1088
408 return (retValue_acc);
409 } else {
410#line 1090
411 if (index == 1) {
412#line 1095
413 retValue_acc = __ste_Client_AddressBook0_Alias1;
414#line 1097
415 return (retValue_acc);
416 } else {
417#line 1099
418 if (index == 2) {
419#line 1104
420 retValue_acc = __ste_Client_AddressBook0_Alias2;
421#line 1106
422 return (retValue_acc);
423 } else {
424#line 1112
425 retValue_acc = 0;
426#line 1114
427 return (retValue_acc);
428 }
429 }
430 }
431 } else {
432#line 1116 "ClientLib.c"
433 if (handle == 2) {
434#line 154 "ClientLib.c"
435 if (index == 0) {
436#line 1124
437 retValue_acc = __ste_Client_AddressBook1_Alias0;
438#line 1126
439 return (retValue_acc);
440 } else {
441#line 1128
442 if (index == 1) {
443#line 1133
444 retValue_acc = __ste_Client_AddressBook1_Alias1;
445#line 1135
446 return (retValue_acc);
447 } else {
448#line 1137
449 if (index == 2) {
450#line 1142
451 retValue_acc = __ste_Client_AddressBook1_Alias2;
452#line 1144
453 return (retValue_acc);
454 } else {
455#line 1150
456 retValue_acc = 0;
457#line 1152
458 return (retValue_acc);
459 }
460 }
461 }
462 } else {
463#line 1154 "ClientLib.c"
464 if (handle == 3) {
465#line 164 "ClientLib.c"
466 if (index == 0) {
467#line 1162
468 retValue_acc = __ste_Client_AddressBook2_Alias0;
469#line 1164
470 return (retValue_acc);
471 } else {
472#line 1166
473 if (index == 1) {
474#line 1171
475 retValue_acc = __ste_Client_AddressBook2_Alias1;
476#line 1173
477 return (retValue_acc);
478 } else {
479#line 1175
480 if (index == 2) {
481#line 1180
482 retValue_acc = __ste_Client_AddressBook2_Alias2;
483#line 1182
484 return (retValue_acc);
485 } else {
486#line 1188
487 retValue_acc = 0;
488#line 1190
489 return (retValue_acc);
490 }
491 }
492 }
493 } else {
494#line 1196 "ClientLib.c"
495 retValue_acc = 0;
496#line 1198
497 return (retValue_acc);
498 }
499 }
500 }
501#line 1205 "ClientLib.c"
502 return (retValue_acc);
503}
504}
505#line 171 "ClientLib.c"
506int findClientAddressBookAlias(int handle , int userid )
507{ int retValue_acc ;
508
509 {
510#line 204
511 if (handle == 1) {
512#line 181 "ClientLib.c"
513 if (userid == __ste_Client_AddressBook0_Alias0) {
514#line 1233
515 retValue_acc = 0;
516#line 1235
517 return (retValue_acc);
518 } else {
519#line 1237
520 if (userid == __ste_Client_AddressBook0_Alias1) {
521#line 1242
522 retValue_acc = 1;
523#line 1244
524 return (retValue_acc);
525 } else {
526#line 1246
527 if (userid == __ste_Client_AddressBook0_Alias2) {
528#line 1251
529 retValue_acc = 2;
530#line 1253
531 return (retValue_acc);
532 } else {
533#line 1259
534 retValue_acc = -1;
535#line 1261
536 return (retValue_acc);
537 }
538 }
539 }
540 } else {
541#line 1263 "ClientLib.c"
542 if (handle == 2) {
543#line 191 "ClientLib.c"
544 if (userid == __ste_Client_AddressBook1_Alias0) {
545#line 1271
546 retValue_acc = 0;
547#line 1273
548 return (retValue_acc);
549 } else {
550#line 1275
551 if (userid == __ste_Client_AddressBook1_Alias1) {
552#line 1280
553 retValue_acc = 1;
554#line 1282
555 return (retValue_acc);
556 } else {
557#line 1284
558 if (userid == __ste_Client_AddressBook1_Alias2) {
559#line 1289
560 retValue_acc = 2;
561#line 1291
562 return (retValue_acc);
563 } else {
564#line 1297
565 retValue_acc = -1;
566#line 1299
567 return (retValue_acc);
568 }
569 }
570 }
571 } else {
572#line 1301 "ClientLib.c"
573 if (handle == 3) {
574#line 201 "ClientLib.c"
575 if (userid == __ste_Client_AddressBook2_Alias0) {
576#line 1309
577 retValue_acc = 0;
578#line 1311
579 return (retValue_acc);
580 } else {
581#line 1313
582 if (userid == __ste_Client_AddressBook2_Alias1) {
583#line 1318
584 retValue_acc = 1;
585#line 1320
586 return (retValue_acc);
587 } else {
588#line 1322
589 if (userid == __ste_Client_AddressBook2_Alias2) {
590#line 1327
591 retValue_acc = 2;
592#line 1329
593 return (retValue_acc);
594 } else {
595#line 1335
596 retValue_acc = -1;
597#line 1337
598 return (retValue_acc);
599 }
600 }
601 }
602 } else {
603#line 1343 "ClientLib.c"
604 retValue_acc = -1;
605#line 1345
606 return (retValue_acc);
607 }
608 }
609 }
610#line 1352 "ClientLib.c"
611 return (retValue_acc);
612}
613}
614#line 208 "ClientLib.c"
615void setClientAddressBookAlias(int handle , int index , int value )
616{
617
618 {
619#line 234
620 if (handle == 1) {
621#line 217
622 if (index == 0) {
623#line 211
624 __ste_Client_AddressBook0_Alias0 = value;
625 } else {
626#line 212
627 if (index == 1) {
628#line 213
629 __ste_Client_AddressBook0_Alias1 = value;
630 } else {
631#line 214
632 if (index == 2) {
633#line 215
634 __ste_Client_AddressBook0_Alias2 = value;
635 } else {
636
637 }
638 }
639 }
640 } else {
641#line 216
642 if (handle == 2) {
643#line 225
644 if (index == 0) {
645#line 219
646 __ste_Client_AddressBook1_Alias0 = value;
647 } else {
648#line 220
649 if (index == 1) {
650#line 221
651 __ste_Client_AddressBook1_Alias1 = value;
652 } else {
653#line 222
654 if (index == 2) {
655#line 223
656 __ste_Client_AddressBook1_Alias2 = value;
657 } else {
658
659 }
660 }
661 }
662 } else {
663#line 224
664 if (handle == 3) {
665#line 233
666 if (index == 0) {
667#line 227
668 __ste_Client_AddressBook2_Alias0 = value;
669 } else {
670#line 228
671 if (index == 1) {
672#line 229
673 __ste_Client_AddressBook2_Alias1 = value;
674 } else {
675#line 230
676 if (index == 2) {
677#line 231
678 __ste_Client_AddressBook2_Alias2 = value;
679 } else {
680
681 }
682 }
683 }
684 } else {
685
686 }
687 }
688 }
689#line 1420 "ClientLib.c"
690 return;
691}
692}
693#line 236 "ClientLib.c"
694int __ste_Client_AddressBook0_Address0 = 0;
695#line 238 "ClientLib.c"
696int __ste_Client_AddressBook0_Address1 = 0;
697#line 240 "ClientLib.c"
698int __ste_Client_AddressBook0_Address2 = 0;
699#line 242 "ClientLib.c"
700int __ste_Client_AddressBook1_Address0 = 0;
701#line 244 "ClientLib.c"
702int __ste_Client_AddressBook1_Address1 = 0;
703#line 246 "ClientLib.c"
704int __ste_Client_AddressBook1_Address2 = 0;
705#line 248 "ClientLib.c"
706int __ste_Client_AddressBook2_Address0 = 0;
707#line 250 "ClientLib.c"
708int __ste_Client_AddressBook2_Address1 = 0;
709#line 252 "ClientLib.c"
710int __ste_Client_AddressBook2_Address2 = 0;
711#line 255 "ClientLib.c"
712int getClientAddressBookAddress(int handle , int index )
713{ int retValue_acc ;
714
715 {
716#line 288
717 if (handle == 1) {
718#line 265 "ClientLib.c"
719 if (index == 0) {
720#line 1462
721 retValue_acc = __ste_Client_AddressBook0_Address0;
722#line 1464
723 return (retValue_acc);
724 } else {
725#line 1466
726 if (index == 1) {
727#line 1471
728 retValue_acc = __ste_Client_AddressBook0_Address1;
729#line 1473
730 return (retValue_acc);
731 } else {
732#line 1475
733 if (index == 2) {
734#line 1480
735 retValue_acc = __ste_Client_AddressBook0_Address2;
736#line 1482
737 return (retValue_acc);
738 } else {
739#line 1488
740 retValue_acc = 0;
741#line 1490
742 return (retValue_acc);
743 }
744 }
745 }
746 } else {
747#line 1492 "ClientLib.c"
748 if (handle == 2) {
749#line 275 "ClientLib.c"
750 if (index == 0) {
751#line 1500
752 retValue_acc = __ste_Client_AddressBook1_Address0;
753#line 1502
754 return (retValue_acc);
755 } else {
756#line 1504
757 if (index == 1) {
758#line 1509
759 retValue_acc = __ste_Client_AddressBook1_Address1;
760#line 1511
761 return (retValue_acc);
762 } else {
763#line 1513
764 if (index == 2) {
765#line 1518
766 retValue_acc = __ste_Client_AddressBook1_Address2;
767#line 1520
768 return (retValue_acc);
769 } else {
770#line 1526
771 retValue_acc = 0;
772#line 1528
773 return (retValue_acc);
774 }
775 }
776 }
777 } else {
778#line 1530 "ClientLib.c"
779 if (handle == 3) {
780#line 285 "ClientLib.c"
781 if (index == 0) {
782#line 1538
783 retValue_acc = __ste_Client_AddressBook2_Address0;
784#line 1540
785 return (retValue_acc);
786 } else {
787#line 1542
788 if (index == 1) {
789#line 1547
790 retValue_acc = __ste_Client_AddressBook2_Address1;
791#line 1549
792 return (retValue_acc);
793 } else {
794#line 1551
795 if (index == 2) {
796#line 1556
797 retValue_acc = __ste_Client_AddressBook2_Address2;
798#line 1558
799 return (retValue_acc);
800 } else {
801#line 1564
802 retValue_acc = 0;
803#line 1566
804 return (retValue_acc);
805 }
806 }
807 }
808 } else {
809#line 1572 "ClientLib.c"
810 retValue_acc = 0;
811#line 1574
812 return (retValue_acc);
813 }
814 }
815 }
816#line 1581 "ClientLib.c"
817 return (retValue_acc);
818}
819}
820#line 291 "ClientLib.c"
821void setClientAddressBookAddress(int handle , int index , int value )
822{
823
824 {
825#line 317
826 if (handle == 1) {
827#line 300
828 if (index == 0) {
829#line 294
830 __ste_Client_AddressBook0_Address0 = value;
831 } else {
832#line 295
833 if (index == 1) {
834#line 296
835 __ste_Client_AddressBook0_Address1 = value;
836 } else {
837#line 297
838 if (index == 2) {
839#line 298
840 __ste_Client_AddressBook0_Address2 = value;
841 } else {
842
843 }
844 }
845 }
846 } else {
847#line 299
848 if (handle == 2) {
849#line 308
850 if (index == 0) {
851#line 302
852 __ste_Client_AddressBook1_Address0 = value;
853 } else {
854#line 303
855 if (index == 1) {
856#line 304
857 __ste_Client_AddressBook1_Address1 = value;
858 } else {
859#line 305
860 if (index == 2) {
861#line 306
862 __ste_Client_AddressBook1_Address2 = value;
863 } else {
864
865 }
866 }
867 }
868 } else {
869#line 307
870 if (handle == 3) {
871#line 316
872 if (index == 0) {
873#line 310
874 __ste_Client_AddressBook2_Address0 = value;
875 } else {
876#line 311
877 if (index == 1) {
878#line 312
879 __ste_Client_AddressBook2_Address1 = value;
880 } else {
881#line 313
882 if (index == 2) {
883#line 314
884 __ste_Client_AddressBook2_Address2 = value;
885 } else {
886
887 }
888 }
889 }
890 } else {
891
892 }
893 }
894 }
895#line 1649 "ClientLib.c"
896 return;
897}
898}
899#line 319 "ClientLib.c"
900int __ste_client_autoResponse0 = 0;
901#line 321 "ClientLib.c"
902int __ste_client_autoResponse1 = 0;
903#line 323 "ClientLib.c"
904int __ste_client_autoResponse2 = 0;
905#line 326 "ClientLib.c"
906int getClientAutoResponse(int handle )
907{ int retValue_acc ;
908
909 {
910#line 335 "ClientLib.c"
911 if (handle == 1) {
912#line 1676
913 retValue_acc = __ste_client_autoResponse0;
914#line 1678
915 return (retValue_acc);
916 } else {
917#line 1680
918 if (handle == 2) {
919#line 1685
920 retValue_acc = __ste_client_autoResponse1;
921#line 1687
922 return (retValue_acc);
923 } else {
924#line 1689
925 if (handle == 3) {
926#line 1694
927 retValue_acc = __ste_client_autoResponse2;
928#line 1696
929 return (retValue_acc);
930 } else {
931#line 1702 "ClientLib.c"
932 retValue_acc = -1;
933#line 1704
934 return (retValue_acc);
935 }
936 }
937 }
938#line 1711 "ClientLib.c"
939 return (retValue_acc);
940}
941}
942#line 338 "ClientLib.c"
943void setClientAutoResponse(int handle , int value )
944{
945
946 {
947#line 346
948 if (handle == 1) {
949#line 340
950 __ste_client_autoResponse0 = value;
951 } else {
952#line 341
953 if (handle == 2) {
954#line 342
955 __ste_client_autoResponse1 = value;
956 } else {
957#line 343
958 if (handle == 3) {
959#line 344
960 __ste_client_autoResponse2 = value;
961 } else {
962
963 }
964 }
965 }
966#line 1746 "ClientLib.c"
967 return;
968}
969}
970#line 348 "ClientLib.c"
971int __ste_client_privateKey0 = 0;
972#line 350 "ClientLib.c"
973int __ste_client_privateKey1 = 0;
974#line 352 "ClientLib.c"
975int __ste_client_privateKey2 = 0;
976#line 355 "ClientLib.c"
977int getClientPrivateKey(int handle )
978{ int retValue_acc ;
979
980 {
981#line 364 "ClientLib.c"
982 if (handle == 1) {
983#line 1773
984 retValue_acc = __ste_client_privateKey0;
985#line 1775
986 return (retValue_acc);
987 } else {
988#line 1777
989 if (handle == 2) {
990#line 1782
991 retValue_acc = __ste_client_privateKey1;
992#line 1784
993 return (retValue_acc);
994 } else {
995#line 1786
996 if (handle == 3) {
997#line 1791
998 retValue_acc = __ste_client_privateKey2;
999#line 1793
1000 return (retValue_acc);
1001 } else {
1002#line 1799 "ClientLib.c"
1003 retValue_acc = 0;
1004#line 1801
1005 return (retValue_acc);
1006 }
1007 }
1008 }
1009#line 1808 "ClientLib.c"
1010 return (retValue_acc);
1011}
1012}
1013#line 367 "ClientLib.c"
1014void setClientPrivateKey(int handle , int value )
1015{
1016
1017 {
1018#line 375
1019 if (handle == 1) {
1020#line 369
1021 __ste_client_privateKey0 = value;
1022 } else {
1023#line 370
1024 if (handle == 2) {
1025#line 371
1026 __ste_client_privateKey1 = value;
1027 } else {
1028#line 372
1029 if (handle == 3) {
1030#line 373
1031 __ste_client_privateKey2 = value;
1032 } else {
1033
1034 }
1035 }
1036 }
1037#line 1843 "ClientLib.c"
1038 return;
1039}
1040}
1041#line 377 "ClientLib.c"
1042int __ste_ClientKeyring_size0 = 0;
1043#line 379 "ClientLib.c"
1044int __ste_ClientKeyring_size1 = 0;
1045#line 381 "ClientLib.c"
1046int __ste_ClientKeyring_size2 = 0;
1047#line 384 "ClientLib.c"
1048int getClientKeyringSize(int handle )
1049{ int retValue_acc ;
1050
1051 {
1052#line 393 "ClientLib.c"
1053 if (handle == 1) {
1054#line 1870
1055 retValue_acc = __ste_ClientKeyring_size0;
1056#line 1872
1057 return (retValue_acc);
1058 } else {
1059#line 1874
1060 if (handle == 2) {
1061#line 1879
1062 retValue_acc = __ste_ClientKeyring_size1;
1063#line 1881
1064 return (retValue_acc);
1065 } else {
1066#line 1883
1067 if (handle == 3) {
1068#line 1888
1069 retValue_acc = __ste_ClientKeyring_size2;
1070#line 1890
1071 return (retValue_acc);
1072 } else {
1073#line 1896 "ClientLib.c"
1074 retValue_acc = 0;
1075#line 1898
1076 return (retValue_acc);
1077 }
1078 }
1079 }
1080#line 1905 "ClientLib.c"
1081 return (retValue_acc);
1082}
1083}
1084#line 396 "ClientLib.c"
1085void setClientKeyringSize(int handle , int value )
1086{
1087
1088 {
1089#line 404
1090 if (handle == 1) {
1091#line 398
1092 __ste_ClientKeyring_size0 = value;
1093 } else {
1094#line 399
1095 if (handle == 2) {
1096#line 400
1097 __ste_ClientKeyring_size1 = value;
1098 } else {
1099#line 401
1100 if (handle == 3) {
1101#line 402
1102 __ste_ClientKeyring_size2 = value;
1103 } else {
1104
1105 }
1106 }
1107 }
1108#line 1940 "ClientLib.c"
1109 return;
1110}
1111}
1112#line 406 "ClientLib.c"
1113int createClientKeyringEntry(int handle )
1114{ int retValue_acc ;
1115 int size ;
1116 int tmp ;
1117 int __cil_tmp5 ;
1118
1119 {
1120 {
1121#line 407
1122 tmp = getClientKeyringSize(handle);
1123#line 407
1124 size = tmp;
1125 }
1126#line 408 "ClientLib.c"
1127 if (size < 2) {
1128 {
1129#line 409 "ClientLib.c"
1130 __cil_tmp5 = size + 1;
1131#line 409
1132 setClientKeyringSize(handle, __cil_tmp5);
1133#line 1967 "ClientLib.c"
1134 retValue_acc = size + 1;
1135 }
1136#line 1969
1137 return (retValue_acc);
1138 } else {
1139#line 1973 "ClientLib.c"
1140 retValue_acc = -1;
1141#line 1975
1142 return (retValue_acc);
1143 }
1144#line 1982 "ClientLib.c"
1145 return (retValue_acc);
1146}
1147}
1148#line 414 "ClientLib.c"
1149int __ste_Client_Keyring0_User0 = 0;
1150#line 416 "ClientLib.c"
1151int __ste_Client_Keyring0_User1 = 0;
1152#line 418 "ClientLib.c"
1153int __ste_Client_Keyring0_User2 = 0;
1154#line 420 "ClientLib.c"
1155int __ste_Client_Keyring1_User0 = 0;
1156#line 422 "ClientLib.c"
1157int __ste_Client_Keyring1_User1 = 0;
1158#line 424 "ClientLib.c"
1159int __ste_Client_Keyring1_User2 = 0;
1160#line 426 "ClientLib.c"
1161int __ste_Client_Keyring2_User0 = 0;
1162#line 428 "ClientLib.c"
1163int __ste_Client_Keyring2_User1 = 0;
1164#line 430 "ClientLib.c"
1165int __ste_Client_Keyring2_User2 = 0;
1166#line 433 "ClientLib.c"
1167int getClientKeyringUser(int handle , int index )
1168{ int retValue_acc ;
1169
1170 {
1171#line 466
1172 if (handle == 1) {
1173#line 443 "ClientLib.c"
1174 if (index == 0) {
1175#line 2028
1176 retValue_acc = __ste_Client_Keyring0_User0;
1177#line 2030
1178 return (retValue_acc);
1179 } else {
1180#line 2032
1181 if (index == 1) {
1182#line 2037
1183 retValue_acc = __ste_Client_Keyring0_User1;
1184#line 2039
1185 return (retValue_acc);
1186 } else {
1187#line 2045
1188 retValue_acc = 0;
1189#line 2047
1190 return (retValue_acc);
1191 }
1192 }
1193 } else {
1194#line 2049 "ClientLib.c"
1195 if (handle == 2) {
1196#line 453 "ClientLib.c"
1197 if (index == 0) {
1198#line 2057
1199 retValue_acc = __ste_Client_Keyring1_User0;
1200#line 2059
1201 return (retValue_acc);
1202 } else {
1203#line 2061
1204 if (index == 1) {
1205#line 2066
1206 retValue_acc = __ste_Client_Keyring1_User1;
1207#line 2068
1208 return (retValue_acc);
1209 } else {
1210#line 2074
1211 retValue_acc = 0;
1212#line 2076
1213 return (retValue_acc);
1214 }
1215 }
1216 } else {
1217#line 2078 "ClientLib.c"
1218 if (handle == 3) {
1219#line 463 "ClientLib.c"
1220 if (index == 0) {
1221#line 2086
1222 retValue_acc = __ste_Client_Keyring2_User0;
1223#line 2088
1224 return (retValue_acc);
1225 } else {
1226#line 2090
1227 if (index == 1) {
1228#line 2095
1229 retValue_acc = __ste_Client_Keyring2_User1;
1230#line 2097
1231 return (retValue_acc);
1232 } else {
1233#line 2103
1234 retValue_acc = 0;
1235#line 2105
1236 return (retValue_acc);
1237 }
1238 }
1239 } else {
1240#line 2111 "ClientLib.c"
1241 retValue_acc = 0;
1242#line 2113
1243 return (retValue_acc);
1244 }
1245 }
1246 }
1247#line 2120 "ClientLib.c"
1248 return (retValue_acc);
1249}
1250}
1251#line 473 "ClientLib.c"
1252void setClientKeyringUser(int handle , int index , int value )
1253{
1254
1255 {
1256#line 499
1257 if (handle == 1) {
1258#line 482
1259 if (index == 0) {
1260#line 476
1261 __ste_Client_Keyring0_User0 = value;
1262 } else {
1263#line 477
1264 if (index == 1) {
1265#line 478
1266 __ste_Client_Keyring0_User1 = value;
1267 } else {
1268
1269 }
1270 }
1271 } else {
1272#line 479
1273 if (handle == 2) {
1274#line 490
1275 if (index == 0) {
1276#line 484
1277 __ste_Client_Keyring1_User0 = value;
1278 } else {
1279#line 485
1280 if (index == 1) {
1281#line 486
1282 __ste_Client_Keyring1_User1 = value;
1283 } else {
1284
1285 }
1286 }
1287 } else {
1288#line 487
1289 if (handle == 3) {
1290#line 498
1291 if (index == 0) {
1292#line 492
1293 __ste_Client_Keyring2_User0 = value;
1294 } else {
1295#line 493
1296 if (index == 1) {
1297#line 494
1298 __ste_Client_Keyring2_User1 = value;
1299 } else {
1300
1301 }
1302 }
1303 } else {
1304
1305 }
1306 }
1307 }
1308#line 2176 "ClientLib.c"
1309 return;
1310}
1311}
1312#line 501 "ClientLib.c"
1313int __ste_Client_Keyring0_PublicKey0 = 0;
1314#line 503 "ClientLib.c"
1315int __ste_Client_Keyring0_PublicKey1 = 0;
1316#line 505 "ClientLib.c"
1317int __ste_Client_Keyring0_PublicKey2 = 0;
1318#line 507 "ClientLib.c"
1319int __ste_Client_Keyring1_PublicKey0 = 0;
1320#line 509 "ClientLib.c"
1321int __ste_Client_Keyring1_PublicKey1 = 0;
1322#line 511 "ClientLib.c"
1323int __ste_Client_Keyring1_PublicKey2 = 0;
1324#line 513 "ClientLib.c"
1325int __ste_Client_Keyring2_PublicKey0 = 0;
1326#line 515 "ClientLib.c"
1327int __ste_Client_Keyring2_PublicKey1 = 0;
1328#line 517 "ClientLib.c"
1329int __ste_Client_Keyring2_PublicKey2 = 0;
1330#line 520 "ClientLib.c"
1331int getClientKeyringPublicKey(int handle , int index )
1332{ int retValue_acc ;
1333
1334 {
1335#line 553
1336 if (handle == 1) {
1337#line 530 "ClientLib.c"
1338 if (index == 0) {
1339#line 2218
1340 retValue_acc = __ste_Client_Keyring0_PublicKey0;
1341#line 2220
1342 return (retValue_acc);
1343 } else {
1344#line 2222
1345 if (index == 1) {
1346#line 2227
1347 retValue_acc = __ste_Client_Keyring0_PublicKey1;
1348#line 2229
1349 return (retValue_acc);
1350 } else {
1351#line 2235
1352 retValue_acc = 0;
1353#line 2237
1354 return (retValue_acc);
1355 }
1356 }
1357 } else {
1358#line 2239 "ClientLib.c"
1359 if (handle == 2) {
1360#line 540 "ClientLib.c"
1361 if (index == 0) {
1362#line 2247
1363 retValue_acc = __ste_Client_Keyring1_PublicKey0;
1364#line 2249
1365 return (retValue_acc);
1366 } else {
1367#line 2251
1368 if (index == 1) {
1369#line 2256
1370 retValue_acc = __ste_Client_Keyring1_PublicKey1;
1371#line 2258
1372 return (retValue_acc);
1373 } else {
1374#line 2264
1375 retValue_acc = 0;
1376#line 2266
1377 return (retValue_acc);
1378 }
1379 }
1380 } else {
1381#line 2268 "ClientLib.c"
1382 if (handle == 3) {
1383#line 550 "ClientLib.c"
1384 if (index == 0) {
1385#line 2276
1386 retValue_acc = __ste_Client_Keyring2_PublicKey0;
1387#line 2278
1388 return (retValue_acc);
1389 } else {
1390#line 2280
1391 if (index == 1) {
1392#line 2285
1393 retValue_acc = __ste_Client_Keyring2_PublicKey1;
1394#line 2287
1395 return (retValue_acc);
1396 } else {
1397#line 2293
1398 retValue_acc = 0;
1399#line 2295
1400 return (retValue_acc);
1401 }
1402 }
1403 } else {
1404#line 2301 "ClientLib.c"
1405 retValue_acc = 0;
1406#line 2303
1407 return (retValue_acc);
1408 }
1409 }
1410 }
1411#line 2310 "ClientLib.c"
1412 return (retValue_acc);
1413}
1414}
1415#line 557 "ClientLib.c"
1416int findPublicKey(int handle , int userid )
1417{ int retValue_acc ;
1418
1419 {
1420#line 591
1421 if (handle == 1) {
1422#line 568 "ClientLib.c"
1423 if (userid == __ste_Client_Keyring0_User0) {
1424#line 2338
1425 retValue_acc = __ste_Client_Keyring0_PublicKey0;
1426#line 2340
1427 return (retValue_acc);
1428 } else {
1429#line 2342
1430 if (userid == __ste_Client_Keyring0_User1) {
1431#line 2347
1432 retValue_acc = __ste_Client_Keyring0_PublicKey1;
1433#line 2349
1434 return (retValue_acc);
1435 } else {
1436#line 2355
1437 retValue_acc = 0;
1438#line 2357
1439 return (retValue_acc);
1440 }
1441 }
1442 } else {
1443#line 2359 "ClientLib.c"
1444 if (handle == 2) {
1445#line 578 "ClientLib.c"
1446 if (userid == __ste_Client_Keyring1_User0) {
1447#line 2367
1448 retValue_acc = __ste_Client_Keyring1_PublicKey0;
1449#line 2369
1450 return (retValue_acc);
1451 } else {
1452#line 2371
1453 if (userid == __ste_Client_Keyring1_User1) {
1454#line 2376
1455 retValue_acc = __ste_Client_Keyring1_PublicKey1;
1456#line 2378
1457 return (retValue_acc);
1458 } else {
1459#line 2384
1460 retValue_acc = 0;
1461#line 2386
1462 return (retValue_acc);
1463 }
1464 }
1465 } else {
1466#line 2388 "ClientLib.c"
1467 if (handle == 3) {
1468#line 588 "ClientLib.c"
1469 if (userid == __ste_Client_Keyring2_User0) {
1470#line 2396
1471 retValue_acc = __ste_Client_Keyring2_PublicKey0;
1472#line 2398
1473 return (retValue_acc);
1474 } else {
1475#line 2400
1476 if (userid == __ste_Client_Keyring2_User1) {
1477#line 2405
1478 retValue_acc = __ste_Client_Keyring2_PublicKey1;
1479#line 2407
1480 return (retValue_acc);
1481 } else {
1482#line 2413
1483 retValue_acc = 0;
1484#line 2415
1485 return (retValue_acc);
1486 }
1487 }
1488 } else {
1489#line 2421 "ClientLib.c"
1490 retValue_acc = 0;
1491#line 2423
1492 return (retValue_acc);
1493 }
1494 }
1495 }
1496#line 2430 "ClientLib.c"
1497 return (retValue_acc);
1498}
1499}
1500#line 595 "ClientLib.c"
1501void setClientKeyringPublicKey(int handle , int index , int value )
1502{
1503
1504 {
1505#line 621
1506 if (handle == 1) {
1507#line 604
1508 if (index == 0) {
1509#line 598
1510 __ste_Client_Keyring0_PublicKey0 = value;
1511 } else {
1512#line 599
1513 if (index == 1) {
1514#line 600
1515 __ste_Client_Keyring0_PublicKey1 = value;
1516 } else {
1517
1518 }
1519 }
1520 } else {
1521#line 601
1522 if (handle == 2) {
1523#line 612
1524 if (index == 0) {
1525#line 606
1526 __ste_Client_Keyring1_PublicKey0 = value;
1527 } else {
1528#line 607
1529 if (index == 1) {
1530#line 608
1531 __ste_Client_Keyring1_PublicKey1 = value;
1532 } else {
1533
1534 }
1535 }
1536 } else {
1537#line 609
1538 if (handle == 3) {
1539#line 620
1540 if (index == 0) {
1541#line 614
1542 __ste_Client_Keyring2_PublicKey0 = value;
1543 } else {
1544#line 615
1545 if (index == 1) {
1546#line 616
1547 __ste_Client_Keyring2_PublicKey1 = value;
1548 } else {
1549
1550 }
1551 }
1552 } else {
1553
1554 }
1555 }
1556 }
1557#line 2486 "ClientLib.c"
1558 return;
1559}
1560}
1561#line 623 "ClientLib.c"
1562int __ste_client_forwardReceiver0 = 0;
1563#line 625 "ClientLib.c"
1564int __ste_client_forwardReceiver1 = 0;
1565#line 627 "ClientLib.c"
1566int __ste_client_forwardReceiver2 = 0;
1567#line 629 "ClientLib.c"
1568int __ste_client_forwardReceiver3 = 0;
1569#line 631 "ClientLib.c"
1570int getClientForwardReceiver(int handle )
1571{ int retValue_acc ;
1572
1573 {
1574#line 640 "ClientLib.c"
1575 if (handle == 1) {
1576#line 2515
1577 retValue_acc = __ste_client_forwardReceiver0;
1578#line 2517
1579 return (retValue_acc);
1580 } else {
1581#line 2519
1582 if (handle == 2) {
1583#line 2524
1584 retValue_acc = __ste_client_forwardReceiver1;
1585#line 2526
1586 return (retValue_acc);
1587 } else {
1588#line 2528
1589 if (handle == 3) {
1590#line 2533
1591 retValue_acc = __ste_client_forwardReceiver2;
1592#line 2535
1593 return (retValue_acc);
1594 } else {
1595#line 2541 "ClientLib.c"
1596 retValue_acc = 0;
1597#line 2543
1598 return (retValue_acc);
1599 }
1600 }
1601 }
1602#line 2550 "ClientLib.c"
1603 return (retValue_acc);
1604}
1605}
1606#line 643 "ClientLib.c"
1607void setClientForwardReceiver(int handle , int value )
1608{
1609
1610 {
1611#line 651
1612 if (handle == 1) {
1613#line 645
1614 __ste_client_forwardReceiver0 = value;
1615 } else {
1616#line 646
1617 if (handle == 2) {
1618#line 647
1619 __ste_client_forwardReceiver1 = value;
1620 } else {
1621#line 648
1622 if (handle == 3) {
1623#line 649
1624 __ste_client_forwardReceiver2 = value;
1625 } else {
1626
1627 }
1628 }
1629 }
1630#line 2585 "ClientLib.c"
1631 return;
1632}
1633}
1634#line 653 "ClientLib.c"
1635int __ste_client_idCounter0 = 0;
1636#line 655 "ClientLib.c"
1637int __ste_client_idCounter1 = 0;
1638#line 657 "ClientLib.c"
1639int __ste_client_idCounter2 = 0;
1640#line 660 "ClientLib.c"
1641int getClientId(int handle )
1642{ int retValue_acc ;
1643
1644 {
1645#line 669 "ClientLib.c"
1646 if (handle == 1) {
1647#line 2612
1648 retValue_acc = __ste_client_idCounter0;
1649#line 2614
1650 return (retValue_acc);
1651 } else {
1652#line 2616
1653 if (handle == 2) {
1654#line 2621
1655 retValue_acc = __ste_client_idCounter1;
1656#line 2623
1657 return (retValue_acc);
1658 } else {
1659#line 2625
1660 if (handle == 3) {
1661#line 2630
1662 retValue_acc = __ste_client_idCounter2;
1663#line 2632
1664 return (retValue_acc);
1665 } else {
1666#line 2638 "ClientLib.c"
1667 retValue_acc = 0;
1668#line 2640
1669 return (retValue_acc);
1670 }
1671 }
1672 }
1673#line 2647 "ClientLib.c"
1674 return (retValue_acc);
1675}
1676}
1677#line 672 "ClientLib.c"
1678void setClientId(int handle , int value )
1679{
1680
1681 {
1682#line 680
1683 if (handle == 1) {
1684#line 674
1685 __ste_client_idCounter0 = value;
1686 } else {
1687#line 675
1688 if (handle == 2) {
1689#line 676
1690 __ste_client_idCounter1 = value;
1691 } else {
1692#line 677
1693 if (handle == 3) {
1694#line 678
1695 __ste_client_idCounter2 = value;
1696 } else {
1697
1698 }
1699 }
1700 }
1701#line 2682 "ClientLib.c"
1702 return;
1703}
1704}
1705#line 1 "Util.o"
1706#pragma merger(0,"Util.i","")
1707#line 359 "/usr/include/stdio.h"
1708extern int printf(char const * __restrict __format , ...) ;
1709#line 1 "Util.h"
1710int prompt(char *msg ) ;
1711#line 9 "Util.c"
1712int prompt(char *msg )
1713{ int retValue_acc ;
1714 int retval ;
1715 char const * __restrict __cil_tmp4 ;
1716
1717 {
1718 {
1719#line 10
1720 __cil_tmp4 = (char const * __restrict )"%s\n";
1721#line 10
1722 printf(__cil_tmp4, msg);
1723#line 518 "Util.c"
1724 retValue_acc = retval;
1725 }
1726#line 520
1727 return (retValue_acc);
1728#line 527
1729 return (retValue_acc);
1730}
1731}
1732#line 1 "EmailLib.o"
1733#pragma merger(0,"EmailLib.i","")
1734#line 4 "EmailLib.h"
1735int initEmail(void) ;
1736#line 6
1737int getEmailId(int handle ) ;
1738#line 8
1739void setEmailId(int handle , int value ) ;
1740#line 10
1741int getEmailFrom(int handle ) ;
1742#line 12
1743void setEmailFrom(int handle , int value ) ;
1744#line 14
1745int getEmailTo(int handle ) ;
1746#line 16
1747void setEmailTo(int handle , int value ) ;
1748#line 18
1749char *getEmailSubject(int handle ) ;
1750#line 20
1751void setEmailSubject(int handle , char *value ) ;
1752#line 22
1753char *getEmailBody(int handle ) ;
1754#line 24
1755void setEmailBody(int handle , char *value ) ;
1756#line 26
1757int isEncrypted(int handle ) ;
1758#line 28
1759void setEmailIsEncrypted(int handle , int value ) ;
1760#line 30
1761int getEmailEncryptionKey(int handle ) ;
1762#line 32
1763void setEmailEncryptionKey(int handle , int value ) ;
1764#line 34
1765int isSigned(int handle ) ;
1766#line 36
1767void setEmailIsSigned(int handle , int value ) ;
1768#line 38
1769int getEmailSignKey(int handle ) ;
1770#line 40
1771void setEmailSignKey(int handle , int value ) ;
1772#line 42
1773int isVerified(int handle ) ;
1774#line 44
1775void setEmailIsSignatureVerified(int handle , int value ) ;
1776#line 5 "EmailLib.c"
1777int __ste_Email_counter = 0;
1778#line 7 "EmailLib.c"
1779int initEmail(void)
1780{ int retValue_acc ;
1781
1782 {
1783#line 12 "EmailLib.c"
1784 if (__ste_Email_counter < 2) {
1785#line 670
1786 __ste_Email_counter = __ste_Email_counter + 1;
1787#line 670
1788 retValue_acc = __ste_Email_counter;
1789#line 672
1790 return (retValue_acc);
1791 } else {
1792#line 678 "EmailLib.c"
1793 retValue_acc = -1;
1794#line 680
1795 return (retValue_acc);
1796 }
1797#line 687 "EmailLib.c"
1798 return (retValue_acc);
1799}
1800}
1801#line 15 "EmailLib.c"
1802int __ste_email_id0 = 0;
1803#line 17 "EmailLib.c"
1804int __ste_email_id1 = 0;
1805#line 19 "EmailLib.c"
1806int getEmailId(int handle )
1807{ int retValue_acc ;
1808
1809 {
1810#line 26 "EmailLib.c"
1811 if (handle == 1) {
1812#line 716
1813 retValue_acc = __ste_email_id0;
1814#line 718
1815 return (retValue_acc);
1816 } else {
1817#line 720
1818 if (handle == 2) {
1819#line 725
1820 retValue_acc = __ste_email_id1;
1821#line 727
1822 return (retValue_acc);
1823 } else {
1824#line 733 "EmailLib.c"
1825 retValue_acc = 0;
1826#line 735
1827 return (retValue_acc);
1828 }
1829 }
1830#line 742 "EmailLib.c"
1831 return (retValue_acc);
1832}
1833}
1834#line 29 "EmailLib.c"
1835void setEmailId(int handle , int value )
1836{
1837
1838 {
1839#line 35
1840 if (handle == 1) {
1841#line 31
1842 __ste_email_id0 = value;
1843 } else {
1844#line 32
1845 if (handle == 2) {
1846#line 33
1847 __ste_email_id1 = value;
1848 } else {
1849
1850 }
1851 }
1852#line 773 "EmailLib.c"
1853 return;
1854}
1855}
1856#line 37 "EmailLib.c"
1857int __ste_email_from0 = 0;
1858#line 39 "EmailLib.c"
1859int __ste_email_from1 = 0;
1860#line 41 "EmailLib.c"
1861int getEmailFrom(int handle )
1862{ int retValue_acc ;
1863
1864 {
1865#line 48 "EmailLib.c"
1866 if (handle == 1) {
1867#line 798
1868 retValue_acc = __ste_email_from0;
1869#line 800
1870 return (retValue_acc);
1871 } else {
1872#line 802
1873 if (handle == 2) {
1874#line 807
1875 retValue_acc = __ste_email_from1;
1876#line 809
1877 return (retValue_acc);
1878 } else {
1879#line 815 "EmailLib.c"
1880 retValue_acc = 0;
1881#line 817
1882 return (retValue_acc);
1883 }
1884 }
1885#line 824 "EmailLib.c"
1886 return (retValue_acc);
1887}
1888}
1889#line 51 "EmailLib.c"
1890void setEmailFrom(int handle , int value )
1891{
1892
1893 {
1894#line 57
1895 if (handle == 1) {
1896#line 53
1897 __ste_email_from0 = value;
1898 } else {
1899#line 54
1900 if (handle == 2) {
1901#line 55
1902 __ste_email_from1 = value;
1903 } else {
1904
1905 }
1906 }
1907#line 855 "EmailLib.c"
1908 return;
1909}
1910}
1911#line 59 "EmailLib.c"
1912int __ste_email_to0 = 0;
1913#line 61 "EmailLib.c"
1914int __ste_email_to1 = 0;
1915#line 63 "EmailLib.c"
1916int getEmailTo(int handle )
1917{ int retValue_acc ;
1918
1919 {
1920#line 70 "EmailLib.c"
1921 if (handle == 1) {
1922#line 880
1923 retValue_acc = __ste_email_to0;
1924#line 882
1925 return (retValue_acc);
1926 } else {
1927#line 884
1928 if (handle == 2) {
1929#line 889
1930 retValue_acc = __ste_email_to1;
1931#line 891
1932 return (retValue_acc);
1933 } else {
1934#line 897 "EmailLib.c"
1935 retValue_acc = 0;
1936#line 899
1937 return (retValue_acc);
1938 }
1939 }
1940#line 906 "EmailLib.c"
1941 return (retValue_acc);
1942}
1943}
1944#line 73 "EmailLib.c"
1945void setEmailTo(int handle , int value )
1946{
1947
1948 {
1949#line 79
1950 if (handle == 1) {
1951#line 75
1952 __ste_email_to0 = value;
1953 } else {
1954#line 76
1955 if (handle == 2) {
1956#line 77
1957 __ste_email_to1 = value;
1958 } else {
1959
1960 }
1961 }
1962#line 937 "EmailLib.c"
1963 return;
1964}
1965}
1966#line 81 "EmailLib.c"
1967char *__ste_email_subject0 ;
1968#line 83 "EmailLib.c"
1969char *__ste_email_subject1 ;
1970#line 85 "EmailLib.c"
1971char *getEmailSubject(int handle )
1972{ char *retValue_acc ;
1973 void *__cil_tmp3 ;
1974
1975 {
1976#line 92 "EmailLib.c"
1977 if (handle == 1) {
1978#line 962
1979 retValue_acc = __ste_email_subject0;
1980#line 964
1981 return (retValue_acc);
1982 } else {
1983#line 966
1984 if (handle == 2) {
1985#line 971
1986 retValue_acc = __ste_email_subject1;
1987#line 973
1988 return (retValue_acc);
1989 } else {
1990#line 979 "EmailLib.c"
1991 __cil_tmp3 = (void *)0;
1992#line 979
1993 retValue_acc = (char *)__cil_tmp3;
1994#line 981
1995 return (retValue_acc);
1996 }
1997 }
1998#line 988 "EmailLib.c"
1999 return (retValue_acc);
2000}
2001}
2002#line 95 "EmailLib.c"
2003void setEmailSubject(int handle , char *value )
2004{
2005
2006 {
2007#line 101
2008 if (handle == 1) {
2009#line 97
2010 __ste_email_subject0 = value;
2011 } else {
2012#line 98
2013 if (handle == 2) {
2014#line 99
2015 __ste_email_subject1 = value;
2016 } else {
2017
2018 }
2019 }
2020#line 1019 "EmailLib.c"
2021 return;
2022}
2023}
2024#line 103 "EmailLib.c"
2025char *__ste_email_body0 = (char *)0;
2026#line 105 "EmailLib.c"
2027char *__ste_email_body1 = (char *)0;
2028#line 107 "EmailLib.c"
2029char *getEmailBody(int handle )
2030{ char *retValue_acc ;
2031 void *__cil_tmp3 ;
2032
2033 {
2034#line 114 "EmailLib.c"
2035 if (handle == 1) {
2036#line 1044
2037 retValue_acc = __ste_email_body0;
2038#line 1046
2039 return (retValue_acc);
2040 } else {
2041#line 1048
2042 if (handle == 2) {
2043#line 1053
2044 retValue_acc = __ste_email_body1;
2045#line 1055
2046 return (retValue_acc);
2047 } else {
2048#line 1061 "EmailLib.c"
2049 __cil_tmp3 = (void *)0;
2050#line 1061
2051 retValue_acc = (char *)__cil_tmp3;
2052#line 1063
2053 return (retValue_acc);
2054 }
2055 }
2056#line 1070 "EmailLib.c"
2057 return (retValue_acc);
2058}
2059}
2060#line 117 "EmailLib.c"
2061void setEmailBody(int handle , char *value )
2062{
2063
2064 {
2065#line 123
2066 if (handle == 1) {
2067#line 119
2068 __ste_email_body0 = value;
2069 } else {
2070#line 120
2071 if (handle == 2) {
2072#line 121
2073 __ste_email_body1 = value;
2074 } else {
2075
2076 }
2077 }
2078#line 1101 "EmailLib.c"
2079 return;
2080}
2081}
2082#line 125 "EmailLib.c"
2083int __ste_email_isEncrypted0 = 0;
2084#line 127 "EmailLib.c"
2085int __ste_email_isEncrypted1 = 0;
2086#line 129 "EmailLib.c"
2087int isEncrypted(int handle )
2088{ int retValue_acc ;
2089
2090 {
2091#line 136 "EmailLib.c"
2092 if (handle == 1) {
2093#line 1126
2094 retValue_acc = __ste_email_isEncrypted0;
2095#line 1128
2096 return (retValue_acc);
2097 } else {
2098#line 1130
2099 if (handle == 2) {
2100#line 1135
2101 retValue_acc = __ste_email_isEncrypted1;
2102#line 1137
2103 return (retValue_acc);
2104 } else {
2105#line 1143 "EmailLib.c"
2106 retValue_acc = 0;
2107#line 1145
2108 return (retValue_acc);
2109 }
2110 }
2111#line 1152 "EmailLib.c"
2112 return (retValue_acc);
2113}
2114}
2115#line 139 "EmailLib.c"
2116void setEmailIsEncrypted(int handle , int value )
2117{
2118
2119 {
2120#line 145
2121 if (handle == 1) {
2122#line 141
2123 __ste_email_isEncrypted0 = value;
2124 } else {
2125#line 142
2126 if (handle == 2) {
2127#line 143
2128 __ste_email_isEncrypted1 = value;
2129 } else {
2130
2131 }
2132 }
2133#line 1183 "EmailLib.c"
2134 return;
2135}
2136}
2137#line 147 "EmailLib.c"
2138int __ste_email_encryptionKey0 = 0;
2139#line 149 "EmailLib.c"
2140int __ste_email_encryptionKey1 = 0;
2141#line 151 "EmailLib.c"
2142int getEmailEncryptionKey(int handle )
2143{ int retValue_acc ;
2144
2145 {
2146#line 158 "EmailLib.c"
2147 if (handle == 1) {
2148#line 1208
2149 retValue_acc = __ste_email_encryptionKey0;
2150#line 1210
2151 return (retValue_acc);
2152 } else {
2153#line 1212
2154 if (handle == 2) {
2155#line 1217
2156 retValue_acc = __ste_email_encryptionKey1;
2157#line 1219
2158 return (retValue_acc);
2159 } else {
2160#line 1225 "EmailLib.c"
2161 retValue_acc = 0;
2162#line 1227
2163 return (retValue_acc);
2164 }
2165 }
2166#line 1234 "EmailLib.c"
2167 return (retValue_acc);
2168}
2169}
2170#line 161 "EmailLib.c"
2171void setEmailEncryptionKey(int handle , int value )
2172{
2173
2174 {
2175#line 167
2176 if (handle == 1) {
2177#line 163
2178 __ste_email_encryptionKey0 = value;
2179 } else {
2180#line 164
2181 if (handle == 2) {
2182#line 165
2183 __ste_email_encryptionKey1 = value;
2184 } else {
2185
2186 }
2187 }
2188#line 1265 "EmailLib.c"
2189 return;
2190}
2191}
2192#line 169 "EmailLib.c"
2193int __ste_email_isSigned0 = 0;
2194#line 171 "EmailLib.c"
2195int __ste_email_isSigned1 = 0;
2196#line 173 "EmailLib.c"
2197int isSigned(int handle )
2198{ int retValue_acc ;
2199
2200 {
2201#line 180 "EmailLib.c"
2202 if (handle == 1) {
2203#line 1290
2204 retValue_acc = __ste_email_isSigned0;
2205#line 1292
2206 return (retValue_acc);
2207 } else {
2208#line 1294
2209 if (handle == 2) {
2210#line 1299
2211 retValue_acc = __ste_email_isSigned1;
2212#line 1301
2213 return (retValue_acc);
2214 } else {
2215#line 1307 "EmailLib.c"
2216 retValue_acc = 0;
2217#line 1309
2218 return (retValue_acc);
2219 }
2220 }
2221#line 1316 "EmailLib.c"
2222 return (retValue_acc);
2223}
2224}
2225#line 183 "EmailLib.c"
2226void setEmailIsSigned(int handle , int value )
2227{
2228
2229 {
2230#line 189
2231 if (handle == 1) {
2232#line 185
2233 __ste_email_isSigned0 = value;
2234 } else {
2235#line 186
2236 if (handle == 2) {
2237#line 187
2238 __ste_email_isSigned1 = value;
2239 } else {
2240
2241 }
2242 }
2243#line 1347 "EmailLib.c"
2244 return;
2245}
2246}
2247#line 191 "EmailLib.c"
2248int __ste_email_signKey0 = 0;
2249#line 193 "EmailLib.c"
2250int __ste_email_signKey1 = 0;
2251#line 195 "EmailLib.c"
2252int getEmailSignKey(int handle )
2253{ int retValue_acc ;
2254
2255 {
2256#line 202 "EmailLib.c"
2257 if (handle == 1) {
2258#line 1372
2259 retValue_acc = __ste_email_signKey0;
2260#line 1374
2261 return (retValue_acc);
2262 } else {
2263#line 1376
2264 if (handle == 2) {
2265#line 1381
2266 retValue_acc = __ste_email_signKey1;
2267#line 1383
2268 return (retValue_acc);
2269 } else {
2270#line 1389 "EmailLib.c"
2271 retValue_acc = 0;
2272#line 1391
2273 return (retValue_acc);
2274 }
2275 }
2276#line 1398 "EmailLib.c"
2277 return (retValue_acc);
2278}
2279}
2280#line 205 "EmailLib.c"
2281void setEmailSignKey(int handle , int value )
2282{
2283
2284 {
2285#line 211
2286 if (handle == 1) {
2287#line 207
2288 __ste_email_signKey0 = value;
2289 } else {
2290#line 208
2291 if (handle == 2) {
2292#line 209
2293 __ste_email_signKey1 = value;
2294 } else {
2295
2296 }
2297 }
2298#line 1429 "EmailLib.c"
2299 return;
2300}
2301}
2302#line 213 "EmailLib.c"
2303int __ste_email_isSignatureVerified0 ;
2304#line 215 "EmailLib.c"
2305int __ste_email_isSignatureVerified1 ;
2306#line 217 "EmailLib.c"
2307int isVerified(int handle )
2308{ int retValue_acc ;
2309
2310 {
2311#line 224 "EmailLib.c"
2312 if (handle == 1) {
2313#line 1454
2314 retValue_acc = __ste_email_isSignatureVerified0;
2315#line 1456
2316 return (retValue_acc);
2317 } else {
2318#line 1458
2319 if (handle == 2) {
2320#line 1463
2321 retValue_acc = __ste_email_isSignatureVerified1;
2322#line 1465
2323 return (retValue_acc);
2324 } else {
2325#line 1471 "EmailLib.c"
2326 retValue_acc = 0;
2327#line 1473
2328 return (retValue_acc);
2329 }
2330 }
2331#line 1480 "EmailLib.c"
2332 return (retValue_acc);
2333}
2334}
2335#line 227 "EmailLib.c"
2336void setEmailIsSignatureVerified(int handle , int value )
2337{
2338
2339 {
2340#line 233
2341 if (handle == 1) {
2342#line 229
2343 __ste_email_isSignatureVerified0 = value;
2344 } else {
2345#line 230
2346 if (handle == 2) {
2347#line 231
2348 __ste_email_isSignatureVerified1 = value;
2349 } else {
2350
2351 }
2352 }
2353#line 1511 "EmailLib.c"
2354 return;
2355}
2356}
2357#line 1 "libacc.o"
2358#pragma merger(0,"libacc.i","")
2359#line 73 "/usr/include/assert.h"
2360extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
2361 char const *__file ,
2362 unsigned int __line ,
2363 char const *__function ) ;
2364#line 471 "/usr/include/stdlib.h"
2365extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
2366#line 488
2367extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
2368#line 32 "libacc.c"
2369void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
2370 int ) ,
2371 int val )
2372{ struct __UTAC__EXCEPTION *excep ;
2373 struct __UTAC__CFLOW_FUNC *cf ;
2374 void *tmp ;
2375 unsigned long __cil_tmp7 ;
2376 unsigned long __cil_tmp8 ;
2377 unsigned long __cil_tmp9 ;
2378 unsigned long __cil_tmp10 ;
2379 unsigned long __cil_tmp11 ;
2380 unsigned long __cil_tmp12 ;
2381 unsigned long __cil_tmp13 ;
2382 unsigned long __cil_tmp14 ;
2383 int (**mem_15)(int , int ) ;
2384 int *mem_16 ;
2385 struct __UTAC__CFLOW_FUNC **mem_17 ;
2386 struct __UTAC__CFLOW_FUNC **mem_18 ;
2387 struct __UTAC__CFLOW_FUNC **mem_19 ;
2388
2389 {
2390 {
2391#line 33
2392 excep = (struct __UTAC__EXCEPTION *)exception;
2393#line 34
2394 tmp = malloc(24UL);
2395#line 34
2396 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
2397#line 36
2398 mem_15 = (int (**)(int , int ))cf;
2399#line 36
2400 *mem_15 = cflow_func;
2401#line 37
2402 __cil_tmp7 = (unsigned long )cf;
2403#line 37
2404 __cil_tmp8 = __cil_tmp7 + 8;
2405#line 37
2406 mem_16 = (int *)__cil_tmp8;
2407#line 37
2408 *mem_16 = val;
2409#line 38
2410 __cil_tmp9 = (unsigned long )cf;
2411#line 38
2412 __cil_tmp10 = __cil_tmp9 + 16;
2413#line 38
2414 __cil_tmp11 = (unsigned long )excep;
2415#line 38
2416 __cil_tmp12 = __cil_tmp11 + 24;
2417#line 38
2418 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
2419#line 38
2420 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
2421#line 38
2422 *mem_17 = *mem_18;
2423#line 39
2424 __cil_tmp13 = (unsigned long )excep;
2425#line 39
2426 __cil_tmp14 = __cil_tmp13 + 24;
2427#line 39
2428 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
2429#line 39
2430 *mem_19 = cf;
2431 }
2432#line 654 "libacc.c"
2433 return;
2434}
2435}
2436#line 44 "libacc.c"
2437void __utac__exception__cf_handler_free(void *exception )
2438{ struct __UTAC__EXCEPTION *excep ;
2439 struct __UTAC__CFLOW_FUNC *cf ;
2440 struct __UTAC__CFLOW_FUNC *tmp ;
2441 unsigned long __cil_tmp5 ;
2442 unsigned long __cil_tmp6 ;
2443 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
2444 unsigned long __cil_tmp8 ;
2445 unsigned long __cil_tmp9 ;
2446 unsigned long __cil_tmp10 ;
2447 unsigned long __cil_tmp11 ;
2448 void *__cil_tmp12 ;
2449 unsigned long __cil_tmp13 ;
2450 unsigned long __cil_tmp14 ;
2451 struct __UTAC__CFLOW_FUNC **mem_15 ;
2452 struct __UTAC__CFLOW_FUNC **mem_16 ;
2453 struct __UTAC__CFLOW_FUNC **mem_17 ;
2454
2455 {
2456#line 45
2457 excep = (struct __UTAC__EXCEPTION *)exception;
2458#line 46
2459 __cil_tmp5 = (unsigned long )excep;
2460#line 46
2461 __cil_tmp6 = __cil_tmp5 + 24;
2462#line 46
2463 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
2464#line 46
2465 cf = *mem_15;
2466 {
2467#line 49
2468 while (1) {
2469 while_0_continue: ;
2470 {
2471#line 49
2472 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
2473#line 49
2474 __cil_tmp8 = (unsigned long )__cil_tmp7;
2475#line 49
2476 __cil_tmp9 = (unsigned long )cf;
2477#line 49
2478 if (__cil_tmp9 != __cil_tmp8) {
2479
2480 } else {
2481 goto while_0_break;
2482 }
2483 }
2484 {
2485#line 50
2486 tmp = cf;
2487#line 51
2488 __cil_tmp10 = (unsigned long )cf;
2489#line 51
2490 __cil_tmp11 = __cil_tmp10 + 16;
2491#line 51
2492 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
2493#line 51
2494 cf = *mem_16;
2495#line 52
2496 __cil_tmp12 = (void *)tmp;
2497#line 52
2498 free(__cil_tmp12);
2499 }
2500 }
2501 while_0_break: ;
2502 }
2503#line 55
2504 __cil_tmp13 = (unsigned long )excep;
2505#line 55
2506 __cil_tmp14 = __cil_tmp13 + 24;
2507#line 55
2508 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
2509#line 55
2510 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
2511#line 694 "libacc.c"
2512 return;
2513}
2514}
2515#line 59 "libacc.c"
2516void __utac__exception__cf_handler_reset(void *exception )
2517{ struct __UTAC__EXCEPTION *excep ;
2518 struct __UTAC__CFLOW_FUNC *cf ;
2519 unsigned long __cil_tmp5 ;
2520 unsigned long __cil_tmp6 ;
2521 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
2522 unsigned long __cil_tmp8 ;
2523 unsigned long __cil_tmp9 ;
2524 int (*__cil_tmp10)(int , int ) ;
2525 unsigned long __cil_tmp11 ;
2526 unsigned long __cil_tmp12 ;
2527 int __cil_tmp13 ;
2528 unsigned long __cil_tmp14 ;
2529 unsigned long __cil_tmp15 ;
2530 struct __UTAC__CFLOW_FUNC **mem_16 ;
2531 int (**mem_17)(int , int ) ;
2532 int *mem_18 ;
2533 struct __UTAC__CFLOW_FUNC **mem_19 ;
2534
2535 {
2536#line 60
2537 excep = (struct __UTAC__EXCEPTION *)exception;
2538#line 61
2539 __cil_tmp5 = (unsigned long )excep;
2540#line 61
2541 __cil_tmp6 = __cil_tmp5 + 24;
2542#line 61
2543 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
2544#line 61
2545 cf = *mem_16;
2546 {
2547#line 64
2548 while (1) {
2549 while_1_continue: ;
2550 {
2551#line 64
2552 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
2553#line 64
2554 __cil_tmp8 = (unsigned long )__cil_tmp7;
2555#line 64
2556 __cil_tmp9 = (unsigned long )cf;
2557#line 64
2558 if (__cil_tmp9 != __cil_tmp8) {
2559
2560 } else {
2561 goto while_1_break;
2562 }
2563 }
2564 {
2565#line 65
2566 mem_17 = (int (**)(int , int ))cf;
2567#line 65
2568 __cil_tmp10 = *mem_17;
2569#line 65
2570 __cil_tmp11 = (unsigned long )cf;
2571#line 65
2572 __cil_tmp12 = __cil_tmp11 + 8;
2573#line 65
2574 mem_18 = (int *)__cil_tmp12;
2575#line 65
2576 __cil_tmp13 = *mem_18;
2577#line 65
2578 (*__cil_tmp10)(4, __cil_tmp13);
2579#line 66
2580 __cil_tmp14 = (unsigned long )cf;
2581#line 66
2582 __cil_tmp15 = __cil_tmp14 + 16;
2583#line 66
2584 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
2585#line 66
2586 cf = *mem_19;
2587 }
2588 }
2589 while_1_break: ;
2590 }
2591 {
2592#line 69
2593 __utac__exception__cf_handler_free(exception);
2594 }
2595#line 732 "libacc.c"
2596 return;
2597}
2598}
2599#line 80 "libacc.c"
2600void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
2601#line 80 "libacc.c"
2602static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
2603#line 79 "libacc.c"
2604void *__utac__error_stack_mgt(void *env , int mode , int count )
2605{ void *retValue_acc ;
2606 struct __ACC__ERR *new ;
2607 void *tmp ;
2608 struct __ACC__ERR *temp ;
2609 struct __ACC__ERR *next ;
2610 void *excep ;
2611 unsigned long __cil_tmp10 ;
2612 unsigned long __cil_tmp11 ;
2613 unsigned long __cil_tmp12 ;
2614 unsigned long __cil_tmp13 ;
2615 void *__cil_tmp14 ;
2616 unsigned long __cil_tmp15 ;
2617 unsigned long __cil_tmp16 ;
2618 void *__cil_tmp17 ;
2619 void **mem_18 ;
2620 struct __ACC__ERR **mem_19 ;
2621 struct __ACC__ERR **mem_20 ;
2622 void **mem_21 ;
2623 struct __ACC__ERR **mem_22 ;
2624 void **mem_23 ;
2625 void **mem_24 ;
2626
2627 {
2628#line 82 "libacc.c"
2629 if (count == 0) {
2630#line 758 "libacc.c"
2631 return (retValue_acc);
2632 } else {
2633
2634 }
2635#line 86 "libacc.c"
2636 if (mode == 0) {
2637 {
2638#line 87
2639 tmp = malloc(16UL);
2640#line 87
2641 new = (struct __ACC__ERR *)tmp;
2642#line 88
2643 mem_18 = (void **)new;
2644#line 88
2645 *mem_18 = env;
2646#line 89
2647 __cil_tmp10 = (unsigned long )new;
2648#line 89
2649 __cil_tmp11 = __cil_tmp10 + 8;
2650#line 89
2651 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
2652#line 89
2653 *mem_19 = head;
2654#line 90
2655 head = new;
2656#line 776 "libacc.c"
2657 retValue_acc = (void *)new;
2658 }
2659#line 778
2660 return (retValue_acc);
2661 } else {
2662
2663 }
2664#line 94 "libacc.c"
2665 if (mode == 1) {
2666#line 95
2667 temp = head;
2668 {
2669#line 98
2670 while (1) {
2671 while_2_continue: ;
2672#line 98
2673 if (count > 1) {
2674
2675 } else {
2676 goto while_2_break;
2677 }
2678 {
2679#line 99
2680 __cil_tmp12 = (unsigned long )temp;
2681#line 99
2682 __cil_tmp13 = __cil_tmp12 + 8;
2683#line 99
2684 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
2685#line 99
2686 next = *mem_20;
2687#line 100
2688 mem_21 = (void **)temp;
2689#line 100
2690 excep = *mem_21;
2691#line 101
2692 __cil_tmp14 = (void *)temp;
2693#line 101
2694 free(__cil_tmp14);
2695#line 102
2696 __utac__exception__cf_handler_reset(excep);
2697#line 103
2698 temp = next;
2699#line 104
2700 count = count - 1;
2701 }
2702 }
2703 while_2_break: ;
2704 }
2705 {
2706#line 107
2707 __cil_tmp15 = (unsigned long )temp;
2708#line 107
2709 __cil_tmp16 = __cil_tmp15 + 8;
2710#line 107
2711 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
2712#line 107
2713 head = *mem_22;
2714#line 108
2715 mem_23 = (void **)temp;
2716#line 108
2717 excep = *mem_23;
2718#line 109
2719 __cil_tmp17 = (void *)temp;
2720#line 109
2721 free(__cil_tmp17);
2722#line 110
2723 __utac__exception__cf_handler_reset(excep);
2724#line 820 "libacc.c"
2725 retValue_acc = excep;
2726 }
2727#line 822
2728 return (retValue_acc);
2729 } else {
2730
2731 }
2732#line 114
2733 if (mode == 2) {
2734#line 118 "libacc.c"
2735 if (head) {
2736#line 831
2737 mem_24 = (void **)head;
2738#line 831
2739 retValue_acc = *mem_24;
2740#line 833
2741 return (retValue_acc);
2742 } else {
2743#line 837 "libacc.c"
2744 retValue_acc = (void *)0;
2745#line 839
2746 return (retValue_acc);
2747 }
2748 } else {
2749
2750 }
2751#line 846 "libacc.c"
2752 return (retValue_acc);
2753}
2754}
2755#line 122 "libacc.c"
2756void *__utac__get_this_arg(int i , struct JoinPoint *this )
2757{ void *retValue_acc ;
2758 unsigned long __cil_tmp4 ;
2759 unsigned long __cil_tmp5 ;
2760 int __cil_tmp6 ;
2761 int __cil_tmp7 ;
2762 unsigned long __cil_tmp8 ;
2763 unsigned long __cil_tmp9 ;
2764 void **__cil_tmp10 ;
2765 void **__cil_tmp11 ;
2766 int *mem_12 ;
2767 void ***mem_13 ;
2768
2769 {
2770#line 123
2771 if (i > 0) {
2772 {
2773#line 123
2774 __cil_tmp4 = (unsigned long )this;
2775#line 123
2776 __cil_tmp5 = __cil_tmp4 + 16;
2777#line 123
2778 mem_12 = (int *)__cil_tmp5;
2779#line 123
2780 __cil_tmp6 = *mem_12;
2781#line 123
2782 if (i <= __cil_tmp6) {
2783
2784 } else {
2785 {
2786#line 123
2787 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2788 123U, "__utac__get_this_arg");
2789 }
2790 }
2791 }
2792 } else {
2793 {
2794#line 123
2795 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2796 123U, "__utac__get_this_arg");
2797 }
2798 }
2799#line 870 "libacc.c"
2800 __cil_tmp7 = i - 1;
2801#line 870
2802 __cil_tmp8 = (unsigned long )this;
2803#line 870
2804 __cil_tmp9 = __cil_tmp8 + 8;
2805#line 870
2806 mem_13 = (void ***)__cil_tmp9;
2807#line 870
2808 __cil_tmp10 = *mem_13;
2809#line 870
2810 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
2811#line 870
2812 retValue_acc = *__cil_tmp11;
2813#line 872
2814 return (retValue_acc);
2815#line 879
2816 return (retValue_acc);
2817}
2818}
2819#line 129 "libacc.c"
2820char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
2821{ char const *retValue_acc ;
2822 unsigned long __cil_tmp4 ;
2823 unsigned long __cil_tmp5 ;
2824 int __cil_tmp6 ;
2825 int __cil_tmp7 ;
2826 unsigned long __cil_tmp8 ;
2827 unsigned long __cil_tmp9 ;
2828 char const **__cil_tmp10 ;
2829 char const **__cil_tmp11 ;
2830 int *mem_12 ;
2831 char const ***mem_13 ;
2832
2833 {
2834#line 131
2835 if (i > 0) {
2836 {
2837#line 131
2838 __cil_tmp4 = (unsigned long )this;
2839#line 131
2840 __cil_tmp5 = __cil_tmp4 + 16;
2841#line 131
2842 mem_12 = (int *)__cil_tmp5;
2843#line 131
2844 __cil_tmp6 = *mem_12;
2845#line 131
2846 if (i <= __cil_tmp6) {
2847
2848 } else {
2849 {
2850#line 131
2851 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2852 131U, "__utac__get_this_argtype");
2853 }
2854 }
2855 }
2856 } else {
2857 {
2858#line 131
2859 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2860 131U, "__utac__get_this_argtype");
2861 }
2862 }
2863#line 903 "libacc.c"
2864 __cil_tmp7 = i - 1;
2865#line 903
2866 __cil_tmp8 = (unsigned long )this;
2867#line 903
2868 __cil_tmp9 = __cil_tmp8 + 24;
2869#line 903
2870 mem_13 = (char const ***)__cil_tmp9;
2871#line 903
2872 __cil_tmp10 = *mem_13;
2873#line 903
2874 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
2875#line 903
2876 retValue_acc = *__cil_tmp11;
2877#line 905
2878 return (retValue_acc);
2879#line 912
2880 return (retValue_acc);
2881}
2882}
2883#line 1 "wsllib_check.o"
2884#pragma merger(0,"wsllib_check.i","")
2885#line 3 "wsllib_check.c"
2886void __automaton_fail(void)
2887{
2888
2889 {
2890 goto ERROR;
2891 ERROR: ;
2892#line 53 "wsllib_check.c"
2893 return;
2894}
2895}
2896#line 1 "featureselect.o"
2897#pragma merger(0,"featureselect.i","")
2898#line 8 "featureselect.h"
2899int __SELECTED_FEATURE_Base ;
2900#line 11 "featureselect.h"
2901int __SELECTED_FEATURE_Keys ;
2902#line 14 "featureselect.h"
2903int __SELECTED_FEATURE_Encrypt ;
2904#line 17 "featureselect.h"
2905int __SELECTED_FEATURE_AutoResponder ;
2906#line 20 "featureselect.h"
2907int __SELECTED_FEATURE_AddressBook ;
2908#line 23 "featureselect.h"
2909int __SELECTED_FEATURE_Sign ;
2910#line 26 "featureselect.h"
2911int __SELECTED_FEATURE_Forward ;
2912#line 29 "featureselect.h"
2913int __SELECTED_FEATURE_Verify ;
2914#line 32 "featureselect.h"
2915int __SELECTED_FEATURE_Decrypt ;
2916#line 35 "featureselect.h"
2917int __GUIDSL_ROOT_PRODUCTION ;
2918#line 37 "featureselect.h"
2919int __GUIDSL_NON_TERMINAL_main ;
2920#line 41
2921int select_one(void) ;
2922#line 43
2923void select_features(void) ;
2924#line 45
2925void select_helpers(void) ;
2926#line 47
2927int valid_product(void) ;
2928#line 8 "featureselect.c"
2929int select_one(void)
2930{ int retValue_acc ;
2931 int choice = __VERIFIER_nondet_int();
2932
2933 {
2934#line 84 "featureselect.c"
2935 retValue_acc = choice;
2936#line 86
2937 return (retValue_acc);
2938#line 93
2939 return (retValue_acc);
2940}
2941}
2942#line 14 "featureselect.c"
2943void select_features(void)
2944{
2945
2946 {
2947#line 115 "featureselect.c"
2948 return;
2949}
2950}
2951#line 20 "featureselect.c"
2952void select_helpers(void)
2953{
2954
2955 {
2956#line 133 "featureselect.c"
2957 return;
2958}
2959}
2960#line 25 "featureselect.c"
2961int valid_product(void)
2962{ int retValue_acc ;
2963
2964 {
2965#line 151 "featureselect.c"
2966 retValue_acc = 1;
2967#line 153
2968 return (retValue_acc);
2969#line 160
2970 return (retValue_acc);
2971}
2972}
2973#line 1 "scenario.o"
2974#pragma merger(0,"scenario.i","")
2975#line 17 "scenario.c"
2976void bobKeyAdd(void) ;
2977#line 24
2978void rjhDeletePrivateKey(void) ;
2979#line 28
2980void rjhKeyAdd(void) ;
2981#line 32
2982void chuckKeyAddRjh(void) ;
2983#line 36
2984void rjhEnableForwarding(void) ;
2985#line 40
2986void rjhKeyChange(void) ;
2987#line 44
2988void bobSetAddressBook(void) ;
2989#line 48
2990void chuckKeyAdd(void) ;
2991#line 52
2992void bobKeyChange(void) ;
2993#line 54
2994#line 61
2995void bobToRjh(void) ;
2996#line 1 "scenario.c"
2997void test(void)
2998{ int op1 ;
2999 int op2 ;
3000 int op3 ;
3001 int op4 ;
3002 int op5 ;
3003 int op6 ;
3004 int op7 ;
3005 int op8 ;
3006 int op9 ;
3007 int op10 ;
3008 int op11 ;
3009 int splverifierCounter ;
3010 int tmp ;
3011 int tmp___0 ;
3012 int tmp___1 ;
3013 int tmp___2 ;
3014 int tmp___3 ;
3015 int tmp___4 ;
3016 int tmp___5 ;
3017 int tmp___6 ;
3018 int tmp___7 ;
3019 int tmp___8 ;
3020 int tmp___9 ;
3021
3022 {
3023#line 2
3024 op1 = 0;
3025#line 3
3026 op2 = 0;
3027#line 4
3028 op3 = 0;
3029#line 5
3030 op4 = 0;
3031#line 6
3032 op5 = 0;
3033#line 7
3034 op6 = 0;
3035#line 8
3036 op7 = 0;
3037#line 9
3038 op8 = 0;
3039#line 10
3040 op9 = 0;
3041#line 11
3042 op10 = 0;
3043#line 12
3044 op11 = 0;
3045#line 13
3046 splverifierCounter = 0;
3047 {
3048#line 14
3049 while (1) {
3050 while_3_continue: ;
3051#line 14
3052 if (splverifierCounter < 4) {
3053
3054 } else {
3055 goto while_3_break;
3056 }
3057#line 15
3058 splverifierCounter = splverifierCounter + 1;
3059#line 16
3060 if (! op1) {
3061 {
3062#line 16
3063 tmp___9 = __VERIFIER_nondet_int();
3064 }
3065#line 16
3066 if (tmp___9) {
3067 {
3068#line 17
3069 bobKeyAdd();
3070#line 18
3071 op1 = 1;
3072 }
3073 } else {
3074 goto _L___8;
3075 }
3076 } else {
3077 _L___8:
3078#line 19
3079 if (! op2) {
3080 {
3081#line 19
3082 tmp___8 = __VERIFIER_nondet_int();
3083 }
3084#line 19
3085 if (tmp___8) {
3086#line 21
3087 op2 = 1;
3088 } else {
3089 goto _L___7;
3090 }
3091 } else {
3092 _L___7:
3093#line 22
3094 if (! op3) {
3095 {
3096#line 22
3097 tmp___7 = __VERIFIER_nondet_int();
3098 }
3099#line 22
3100 if (tmp___7) {
3101 {
3102#line 24
3103 rjhDeletePrivateKey();
3104#line 25
3105 op3 = 1;
3106 }
3107 } else {
3108 goto _L___6;
3109 }
3110 } else {
3111 _L___6:
3112#line 26
3113 if (! op4) {
3114 {
3115#line 26
3116 tmp___6 = __VERIFIER_nondet_int();
3117 }
3118#line 26
3119 if (tmp___6) {
3120 {
3121#line 28
3122 rjhKeyAdd();
3123#line 29
3124 op4 = 1;
3125 }
3126 } else {
3127 goto _L___5;
3128 }
3129 } else {
3130 _L___5:
3131#line 30
3132 if (! op5) {
3133 {
3134#line 30
3135 tmp___5 = __VERIFIER_nondet_int();
3136 }
3137#line 30
3138 if (tmp___5) {
3139 {
3140#line 32
3141 chuckKeyAddRjh();
3142#line 33
3143 op5 = 1;
3144 }
3145 } else {
3146 goto _L___4;
3147 }
3148 } else {
3149 _L___4:
3150#line 34
3151 if (! op6) {
3152 {
3153#line 34
3154 tmp___4 = __VERIFIER_nondet_int();
3155 }
3156#line 34
3157 if (tmp___4) {
3158 {
3159#line 36
3160 rjhEnableForwarding();
3161#line 37
3162 op6 = 1;
3163 }
3164 } else {
3165 goto _L___3;
3166 }
3167 } else {
3168 _L___3:
3169#line 38
3170 if (! op7) {
3171 {
3172#line 38
3173 tmp___3 = __VERIFIER_nondet_int();
3174 }
3175#line 38
3176 if (tmp___3) {
3177 {
3178#line 40
3179 rjhKeyChange();
3180#line 41
3181 op7 = 1;
3182 }
3183 } else {
3184 goto _L___2;
3185 }
3186 } else {
3187 _L___2:
3188#line 42
3189 if (! op8) {
3190 {
3191#line 42
3192 tmp___2 = __VERIFIER_nondet_int();
3193 }
3194#line 42
3195 if (tmp___2) {
3196 {
3197#line 44
3198 bobSetAddressBook();
3199#line 45
3200 op8 = 1;
3201 }
3202 } else {
3203 goto _L___1;
3204 }
3205 } else {
3206 _L___1:
3207#line 46
3208 if (! op9) {
3209 {
3210#line 46
3211 tmp___1 = __VERIFIER_nondet_int();
3212 }
3213#line 46
3214 if (tmp___1) {
3215 {
3216#line 48
3217 chuckKeyAdd();
3218#line 49
3219 op9 = 1;
3220 }
3221 } else {
3222 goto _L___0;
3223 }
3224 } else {
3225 _L___0:
3226#line 50
3227 if (! op10) {
3228 {
3229#line 50
3230 tmp___0 = __VERIFIER_nondet_int();
3231 }
3232#line 50
3233 if (tmp___0) {
3234 {
3235#line 52
3236 bobKeyChange();
3237#line 53
3238 op10 = 1;
3239 }
3240 } else {
3241 goto _L;
3242 }
3243 } else {
3244 _L:
3245#line 54
3246 if (! op11) {
3247 {
3248#line 54
3249 tmp = __VERIFIER_nondet_int();
3250 }
3251#line 54
3252 if (tmp) {
3253 {
3254#line 56
3255 chuckKeyAdd();
3256#line 57
3257 op11 = 1;
3258 }
3259 } else {
3260 goto while_3_break;
3261 }
3262 } else {
3263 goto while_3_break;
3264 }
3265 }
3266 }
3267 }
3268 }
3269 }
3270 }
3271 }
3272 }
3273 }
3274 }
3275 }
3276 while_3_break: ;
3277 }
3278 {
3279#line 61
3280 bobToRjh();
3281 }
3282#line 169 "scenario.c"
3283 return;
3284}
3285}
3286#line 1 "DecryptForward_spec.o"
3287#pragma merger(0,"DecryptForward_spec.i","")
3288#line 9 "Email.h"
3289int isReadable(int msg ) ;
3290#line 688 "/usr/include/stdio.h"
3291extern int puts(char const *__s ) ;
3292#line 11 "DecryptForward_spec.c"
3293__inline void __utac_acc__DecryptForward_spec__1(int msg )
3294{ int tmp ;
3295
3296 {
3297 {
3298#line 13
3299 puts("before forward\n");
3300#line 14
3301 tmp = isReadable(msg);
3302 }
3303#line 14
3304 if (tmp) {
3305
3306 } else {
3307 {
3308#line 15
3309 __automaton_fail();
3310 }
3311 }
3312#line 15
3313 return;
3314}
3315}
3316#line 1 "Test.o"
3317#pragma merger(0,"Test.i","")
3318#line 17 "Client.h"
3319int is_queue_empty(void) ;
3320#line 19
3321int get_queued_client(void) ;
3322#line 21
3323int get_queued_email(void) ;
3324#line 26
3325void outgoing(int client , int msg ) ;
3326#line 35
3327void sendEmail(int sender , int receiver ) ;
3328#line 44
3329void generateKeyPair(int client , int seed ) ;
3330#line 2 "Test.h"
3331int bob ;
3332#line 5 "Test.h"
3333int rjh ;
3334#line 8 "Test.h"
3335int chuck ;
3336#line 11
3337void setup_bob(int bob___0 ) ;
3338#line 14
3339void setup_rjh(int rjh___0 ) ;
3340#line 17
3341void setup_chuck(int chuck___0 ) ;
3342#line 26
3343void rjhToBob(void) ;
3344#line 32
3345void setup(void) ;
3346#line 35
3347int main(void) ;
3348#line 39
3349void bobKeyAddChuck(void) ;
3350#line 45
3351void rjhKeyAddChuck(void) ;
3352#line 18 "Test.c"
3353void setup_bob__wrappee__Base(int bob___0 )
3354{
3355
3356 {
3357 {
3358#line 19
3359 setClientId(bob___0, bob___0);
3360 }
3361#line 1330 "Test.c"
3362 return;
3363}
3364}
3365#line 23 "Test.c"
3366void setup_bob(int bob___0 )
3367{
3368
3369 {
3370 {
3371#line 24
3372 setup_bob__wrappee__Base(bob___0);
3373#line 25
3374 setClientPrivateKey(bob___0, 123);
3375 }
3376#line 1352 "Test.c"
3377 return;
3378}
3379}
3380#line 33 "Test.c"
3381void setup_rjh__wrappee__Base(int rjh___0 )
3382{
3383
3384 {
3385 {
3386#line 34
3387 setClientId(rjh___0, rjh___0);
3388 }
3389#line 1372 "Test.c"
3390 return;
3391}
3392}
3393#line 40 "Test.c"
3394void setup_rjh(int rjh___0 )
3395{
3396
3397 {
3398 {
3399#line 42
3400 setup_rjh__wrappee__Base(rjh___0);
3401#line 43
3402 setClientPrivateKey(rjh___0, 456);
3403 }
3404#line 1394 "Test.c"
3405 return;
3406}
3407}
3408#line 50 "Test.c"
3409void setup_chuck__wrappee__Base(int chuck___0 )
3410{
3411
3412 {
3413 {
3414#line 51
3415 setClientId(chuck___0, chuck___0);
3416 }
3417#line 1414 "Test.c"
3418 return;
3419}
3420}
3421#line 57 "Test.c"
3422void setup_chuck(int chuck___0 )
3423{
3424
3425 {
3426 {
3427#line 58
3428 setup_chuck__wrappee__Base(chuck___0);
3429#line 59
3430 setClientPrivateKey(chuck___0, 789);
3431 }
3432#line 1436 "Test.c"
3433 return;
3434}
3435}
3436#line 69 "Test.c"
3437void bobToRjh(void)
3438{ int tmp ;
3439 int tmp___0 ;
3440 int tmp___1 ;
3441
3442 {
3443 {
3444#line 71
3445 puts("Please enter a subject and a message body.\n");
3446#line 72
3447 sendEmail(bob, rjh);
3448#line 73
3449 tmp___1 = is_queue_empty();
3450 }
3451#line 73
3452 if (tmp___1) {
3453
3454 } else {
3455 {
3456#line 74
3457 tmp = get_queued_email();
3458#line 74
3459 tmp___0 = get_queued_client();
3460#line 74
3461 outgoing(tmp___0, tmp);
3462 }
3463 }
3464#line 1463 "Test.c"
3465 return;
3466}
3467}
3468#line 81 "Test.c"
3469void rjhToBob(void)
3470{
3471
3472 {
3473 {
3474#line 83
3475 puts("Please enter a subject and a message body.\n");
3476#line 84
3477 sendEmail(rjh, bob);
3478 }
3479#line 1485 "Test.c"
3480 return;
3481}
3482}
3483#line 88 "Test.c"
3484#line 95 "Test.c"
3485void setup(void)
3486{ char const * __restrict __cil_tmp1 ;
3487 char const * __restrict __cil_tmp2 ;
3488 char const * __restrict __cil_tmp3 ;
3489
3490 {
3491 {
3492#line 96
3493 bob = 1;
3494#line 97
3495 setup_bob(bob);
3496#line 98
3497 __cil_tmp1 = (char const * __restrict )"bob: %d\n";
3498#line 98
3499 printf(__cil_tmp1, bob);
3500#line 100
3501 rjh = 2;
3502#line 101
3503 setup_rjh(rjh);
3504#line 102
3505 __cil_tmp2 = (char const * __restrict )"rjh: %d\n";
3506#line 102
3507 printf(__cil_tmp2, rjh);
3508#line 104
3509 chuck = 3;
3510#line 105
3511 setup_chuck(chuck);
3512#line 106
3513 __cil_tmp3 = (char const * __restrict )"chuck: %d\n";
3514#line 106
3515 printf(__cil_tmp3, chuck);
3516 }
3517#line 1556 "Test.c"
3518 return;
3519}
3520}
3521#line 112 "Test.c"
3522int main(void)
3523{ int retValue_acc ;
3524 int tmp ;
3525
3526 {
3527 {
3528#line 113
3529 select_helpers();
3530#line 114
3531 select_features();
3532#line 115
3533 tmp = valid_product();
3534 }
3535#line 115
3536 if (tmp) {
3537 {
3538#line 116
3539 setup();
3540#line 117
3541 test();
3542 }
3543 } else {
3544
3545 }
3546#line 1587 "Test.c"
3547 return (retValue_acc);
3548}
3549}
3550#line 125 "Test.c"
3551void bobKeyAdd(void)
3552{ int tmp ;
3553 int tmp___0 ;
3554 char const * __restrict __cil_tmp3 ;
3555 char const * __restrict __cil_tmp4 ;
3556
3557 {
3558 {
3559#line 126
3560 createClientKeyringEntry(bob);
3561#line 127
3562 setClientKeyringUser(bob, 0, 2);
3563#line 128
3564 setClientKeyringPublicKey(bob, 0, 456);
3565#line 129
3566 puts("bob added rjhs key");
3567#line 130
3568 tmp = getClientKeyringUser(bob, 0);
3569#line 130
3570 __cil_tmp3 = (char const * __restrict )"%d\n";
3571#line 130
3572 printf(__cil_tmp3, tmp);
3573#line 131
3574 tmp___0 = getClientKeyringPublicKey(bob, 0);
3575#line 131
3576 __cil_tmp4 = (char const * __restrict )"%d\n";
3577#line 131
3578 printf(__cil_tmp4, tmp___0);
3579 }
3580#line 1621 "Test.c"
3581 return;
3582}
3583}
3584#line 137 "Test.c"
3585void rjhKeyAdd(void)
3586{
3587
3588 {
3589 {
3590#line 138
3591 createClientKeyringEntry(rjh);
3592#line 139
3593 setClientKeyringUser(rjh, 0, 1);
3594#line 140
3595 setClientKeyringPublicKey(rjh, 0, 123);
3596 }
3597#line 1645 "Test.c"
3598 return;
3599}
3600}
3601#line 146 "Test.c"
3602void rjhKeyAddChuck(void)
3603{
3604
3605 {
3606 {
3607#line 147
3608 createClientKeyringEntry(rjh);
3609#line 148
3610 setClientKeyringUser(rjh, 0, 3);
3611#line 149
3612 setClientKeyringPublicKey(rjh, 0, 789);
3613 }
3614#line 1669 "Test.c"
3615 return;
3616}
3617}
3618#line 156 "Test.c"
3619void bobKeyAddChuck(void)
3620{
3621
3622 {
3623 {
3624#line 157
3625 createClientKeyringEntry(bob);
3626#line 158
3627 setClientKeyringUser(bob, 1, 3);
3628#line 159
3629 setClientKeyringPublicKey(bob, 1, 789);
3630 }
3631#line 1693 "Test.c"
3632 return;
3633}
3634}
3635#line 165 "Test.c"
3636void chuckKeyAdd(void)
3637{
3638
3639 {
3640 {
3641#line 166
3642 createClientKeyringEntry(chuck);
3643#line 167
3644 setClientKeyringUser(chuck, 0, 1);
3645#line 168
3646 setClientKeyringPublicKey(chuck, 0, 123);
3647 }
3648#line 1717 "Test.c"
3649 return;
3650}
3651}
3652#line 174 "Test.c"
3653void chuckKeyAddRjh(void)
3654{
3655
3656 {
3657 {
3658#line 175
3659 createClientKeyringEntry(chuck);
3660#line 176
3661 setClientKeyringUser(chuck, 0, 2);
3662#line 177
3663 setClientKeyringPublicKey(chuck, 0, 456);
3664 }
3665#line 1741 "Test.c"
3666 return;
3667}
3668}
3669#line 183 "Test.c"
3670void rjhDeletePrivateKey(void)
3671{
3672
3673 {
3674 {
3675#line 184
3676 setClientPrivateKey(rjh, 0);
3677 }
3678#line 1761 "Test.c"
3679 return;
3680}
3681}
3682#line 190 "Test.c"
3683void bobKeyChange(void)
3684{
3685
3686 {
3687 {
3688#line 191
3689 generateKeyPair(bob, 777);
3690 }
3691#line 1781 "Test.c"
3692 return;
3693}
3694}
3695#line 197 "Test.c"
3696void rjhKeyChange(void)
3697{
3698
3699 {
3700 {
3701#line 198
3702 generateKeyPair(rjh, 666);
3703 }
3704#line 1801 "Test.c"
3705 return;
3706}
3707}
3708#line 203 "Test.c"
3709void bobSetAddressBook(void)
3710{
3711
3712 {
3713 {
3714#line 204
3715 setClientAddressBookSize(bob, 1);
3716#line 205
3717 setClientAddressBookAlias(bob, 0, rjh);
3718#line 206
3719 setClientAddressBookAddress(bob, 0, rjh);
3720#line 207
3721 setClientAddressBookAddress(bob, 1, chuck);
3722 }
3723#line 1827 "Test.c"
3724 return;
3725}
3726}
3727#line 213 "Test.c"
3728void rjhEnableForwarding(void)
3729{
3730
3731 {
3732 {
3733#line 214
3734 setClientForwardReceiver(rjh, chuck);
3735 }
3736#line 1847 "Test.c"
3737 return;
3738}
3739}
3740#line 1 "Client.o"
3741#pragma merger(0,"Client.i","")
3742#line 6 "Email.h"
3743void printMail(int msg ) ;
3744#line 12
3745int createEmail(int from , int to ) ;
3746#line 14 "Client.h"
3747void queue(int client , int msg ) ;
3748#line 24
3749void mail(int client , int msg ) ;
3750#line 28
3751void deliver(int client , int msg ) ;
3752#line 30
3753void incoming(int client , int msg ) ;
3754#line 32
3755int createClient(char *name ) ;
3756#line 40
3757int isKeyPairValid(int publicKey , int privateKey ) ;
3758#line 45
3759void sendToAddressBook(int client , int msg ) ;
3760#line 47
3761void forward(int client , int msg ) ;
3762#line 6 "Client.c"
3763int queue_empty = 1;
3764#line 9 "Client.c"
3765int queued_message ;
3766#line 12 "Client.c"
3767int queued_client ;
3768#line 18 "Client.c"
3769void mail(int client , int msg )
3770{ int tmp ;
3771
3772 {
3773 {
3774#line 19
3775 puts("mail sent");
3776#line 20
3777 tmp = getEmailTo(msg);
3778#line 20
3779 incoming(tmp, msg);
3780 }
3781#line 733 "Client.c"
3782 return;
3783}
3784}
3785#line 27 "Client.c"
3786void outgoing__wrappee__Keys(int client , int msg )
3787{ int tmp ;
3788
3789 {
3790 {
3791#line 28
3792 tmp = getClientId(client);
3793#line 28
3794 setEmailFrom(msg, tmp);
3795#line 29
3796 mail(client, msg);
3797 }
3798#line 755 "Client.c"
3799 return;
3800}
3801}
3802#line 33 "Client.c"
3803void outgoing__wrappee__Encrypt(int client , int msg )
3804{ int receiver ;
3805 int tmp ;
3806 int pubkey ;
3807 int tmp___0 ;
3808
3809 {
3810 {
3811#line 36
3812 tmp = getEmailTo(msg);
3813#line 36
3814 receiver = tmp;
3815#line 37
3816 tmp___0 = findPublicKey(client, receiver);
3817#line 37
3818 pubkey = tmp___0;
3819 }
3820#line 38
3821 if (pubkey) {
3822 {
3823#line 39
3824 setEmailEncryptionKey(msg, pubkey);
3825#line 40
3826 setEmailIsEncrypted(msg, 1);
3827 }
3828 } else {
3829
3830 }
3831 {
3832#line 45
3833 outgoing__wrappee__Keys(client, msg);
3834 }
3835#line 790 "Client.c"
3836 return;
3837}
3838}
3839#line 52 "Client.c"
3840void outgoing(int client , int msg )
3841{ int size ;
3842 int tmp ;
3843 int receiver ;
3844 int tmp___0 ;
3845 int second ;
3846 int tmp___1 ;
3847 int tmp___2 ;
3848
3849 {
3850 {
3851#line 54
3852 tmp = getClientAddressBookSize(client);
3853#line 54
3854 size = tmp;
3855 }
3856#line 56
3857 if (size) {
3858 {
3859#line 57
3860 sendToAddressBook(client, msg);
3861#line 58
3862 puts("sending to alias in address book\n");
3863#line 59
3864 tmp___0 = getEmailTo(msg);
3865#line 59
3866 receiver = tmp___0;
3867#line 61
3868 puts("sending to second receipient\n");
3869#line 62
3870 tmp___1 = getClientAddressBookAddress(client, 1);
3871#line 62
3872 second = tmp___1;
3873#line 63
3874 setEmailTo(msg, second);
3875#line 64
3876 outgoing__wrappee__Encrypt(client, msg);
3877#line 67
3878 tmp___2 = getClientAddressBookAddress(client, 0);
3879#line 67
3880 setEmailTo(msg, tmp___2);
3881#line 68
3882 outgoing__wrappee__Encrypt(client, msg);
3883 }
3884 } else {
3885 {
3886#line 70
3887 outgoing__wrappee__Encrypt(client, msg);
3888 }
3889 }
3890#line 840 "Client.c"
3891 return;
3892}
3893}
3894#line 79 "Client.c"
3895void deliver(int client , int msg )
3896{
3897
3898 {
3899 {
3900#line 80
3901 puts("mail delivered\n");
3902 }
3903#line 860 "Client.c"
3904 return;
3905}
3906}
3907#line 87 "Client.c"
3908void incoming__wrappee__AddressBook(int client , int msg )
3909{
3910
3911 {
3912 {
3913#line 88
3914 deliver(client, msg);
3915 }
3916#line 880 "Client.c"
3917 return;
3918}
3919}
3920#line 94 "Client.c"
3921void incoming__wrappee__Forward(int client , int msg )
3922{ int fwreceiver ;
3923 int tmp ;
3924
3925 {
3926 {
3927#line 95
3928 incoming__wrappee__AddressBook(client, msg);
3929#line 96
3930 tmp = getClientForwardReceiver(client);
3931#line 96
3932 fwreceiver = tmp;
3933 }
3934#line 97
3935 if (fwreceiver) {
3936 {
3937#line 99
3938 setEmailTo(msg, fwreceiver);
3939#line 100
3940 forward(client, msg);
3941 }
3942 } else {
3943
3944 }
3945#line 911 "Client.c"
3946 return;
3947}
3948}
3949#line 107 "Client.c"
3950void incoming(int client , int msg )
3951{ int privkey ;
3952 int tmp ;
3953 int tmp___0 ;
3954 int tmp___1 ;
3955 int tmp___2 ;
3956
3957 {
3958 {
3959#line 110
3960 tmp = getClientPrivateKey(client);
3961#line 110
3962 privkey = tmp;
3963 }
3964#line 111
3965 if (privkey) {
3966 {
3967#line 119
3968 tmp___0 = isEncrypted(msg);
3969 }
3970#line 119
3971 if (tmp___0) {
3972 {
3973#line 119
3974 tmp___1 = getEmailEncryptionKey(msg);
3975#line 119
3976 tmp___2 = isKeyPairValid(tmp___1, privkey);
3977 }
3978#line 119
3979 if (tmp___2) {
3980 {
3981#line 116
3982 setEmailIsEncrypted(msg, 0);
3983#line 117
3984 setEmailEncryptionKey(msg, 0);
3985 }
3986 } else {
3987
3988 }
3989 } else {
3990
3991 }
3992 } else {
3993
3994 }
3995 {
3996#line 122
3997 incoming__wrappee__Forward(client, msg);
3998 }
3999#line 945 "Client.c"
4000 return;
4001}
4002}
4003#line 126 "Client.c"
4004int createClient(char *name )
4005{ int retValue_acc ;
4006 int client ;
4007 int tmp ;
4008
4009 {
4010 {
4011#line 127
4012 tmp = initClient();
4013#line 127
4014 client = tmp;
4015#line 967 "Client.c"
4016 retValue_acc = client;
4017 }
4018#line 969
4019 return (retValue_acc);
4020#line 976
4021 return (retValue_acc);
4022}
4023}
4024#line 134 "Client.c"
4025void sendEmail(int sender , int receiver )
4026{ int email ;
4027 int tmp ;
4028
4029 {
4030 {
4031#line 135
4032 tmp = createEmail(0, receiver);
4033#line 135
4034 email = tmp;
4035#line 136
4036 outgoing(sender, email);
4037 }
4038#line 1004 "Client.c"
4039 return;
4040}
4041}
4042#line 144 "Client.c"
4043void queue(int client , int msg )
4044{
4045
4046 {
4047#line 145
4048 queue_empty = 0;
4049#line 146
4050 queued_message = msg;
4051#line 147
4052 queued_client = client;
4053#line 1028 "Client.c"
4054 return;
4055}
4056}
4057#line 153 "Client.c"
4058int is_queue_empty(void)
4059{ int retValue_acc ;
4060
4061 {
4062#line 1046 "Client.c"
4063 retValue_acc = queue_empty;
4064#line 1048
4065 return (retValue_acc);
4066#line 1055
4067 return (retValue_acc);
4068}
4069}
4070#line 160 "Client.c"
4071int get_queued_client(void)
4072{ int retValue_acc ;
4073
4074 {
4075#line 1077 "Client.c"
4076 retValue_acc = queued_client;
4077#line 1079
4078 return (retValue_acc);
4079#line 1086
4080 return (retValue_acc);
4081}
4082}
4083#line 167 "Client.c"
4084int get_queued_email(void)
4085{ int retValue_acc ;
4086
4087 {
4088#line 1108 "Client.c"
4089 retValue_acc = queued_message;
4090#line 1110
4091 return (retValue_acc);
4092#line 1117
4093 return (retValue_acc);
4094}
4095}
4096#line 173 "Client.c"
4097int isKeyPairValid(int publicKey , int privateKey )
4098{ int retValue_acc ;
4099 char const * __restrict __cil_tmp4 ;
4100
4101 {
4102 {
4103#line 174
4104 __cil_tmp4 = (char const * __restrict )"keypair valid %d %d";
4105#line 174
4106 printf(__cil_tmp4, publicKey, privateKey);
4107 }
4108#line 175 "Client.c"
4109 if (! publicKey) {
4110#line 1142 "Client.c"
4111 retValue_acc = 0;
4112#line 1144
4113 return (retValue_acc);
4114 } else {
4115#line 175 "Client.c"
4116 if (! privateKey) {
4117#line 1142 "Client.c"
4118 retValue_acc = 0;
4119#line 1144
4120 return (retValue_acc);
4121 } else {
4122
4123 }
4124 }
4125#line 1149 "Client.c"
4126 retValue_acc = privateKey == publicKey;
4127#line 1151
4128 return (retValue_acc);
4129#line 1158
4130 return (retValue_acc);
4131}
4132}
4133#line 183 "Client.c"
4134void generateKeyPair(int client , int seed )
4135{
4136
4137 {
4138 {
4139#line 184
4140 setClientPrivateKey(client, seed);
4141 }
4142#line 1182 "Client.c"
4143 return;
4144}
4145}
4146#line 189 "Client.c"
4147void sendToAddressBook(int client , int msg )
4148{
4149
4150 {
4151#line 1200 "Client.c"
4152 return;
4153}
4154}
4155#line 195 "Client.c"
4156void forward(int client , int msg )
4157{ int __utac__ad__arg1 ;
4158
4159 {
4160 {
4161#line 1213 "Client.c"
4162 __utac__ad__arg1 = msg;
4163#line 1214
4164 __utac_acc__DecryptForward_spec__1(__utac__ad__arg1);
4165#line 196 "Client.c"
4166 puts("Forwarding message.\n");
4167#line 197
4168 printMail(msg);
4169#line 198
4170 queue(client, msg);
4171 }
4172#line 1233 "Client.c"
4173 return;
4174}
4175}
4176#line 1 "Email.o"
4177#pragma merger(0,"Email.i","")
4178#line 15 "Email.h"
4179int cloneEmail(int msg ) ;
4180#line 9 "Email.c"
4181void printMail__wrappee__Keys(int msg )
4182{ int tmp ;
4183 int tmp___0 ;
4184 int tmp___1 ;
4185 int tmp___2 ;
4186 char const * __restrict __cil_tmp6 ;
4187 char const * __restrict __cil_tmp7 ;
4188 char const * __restrict __cil_tmp8 ;
4189 char const * __restrict __cil_tmp9 ;
4190
4191 {
4192 {
4193#line 10
4194 tmp = getEmailId(msg);
4195#line 10
4196 __cil_tmp6 = (char const * __restrict )"ID:\n %i\n";
4197#line 10
4198 printf(__cil_tmp6, tmp);
4199#line 11
4200 tmp___0 = getEmailFrom(msg);
4201#line 11
4202 __cil_tmp7 = (char const * __restrict )"FROM:\n %i\n";
4203#line 11
4204 printf(__cil_tmp7, tmp___0);
4205#line 12
4206 tmp___1 = getEmailTo(msg);
4207#line 12
4208 __cil_tmp8 = (char const * __restrict )"TO:\n %i\n";
4209#line 12
4210 printf(__cil_tmp8, tmp___1);
4211#line 13
4212 tmp___2 = isReadable(msg);
4213#line 13
4214 __cil_tmp9 = (char const * __restrict )"IS_READABLE\n %i\n";
4215#line 13
4216 printf(__cil_tmp9, tmp___2);
4217 }
4218#line 601 "Email.c"
4219 return;
4220}
4221}
4222#line 17 "Email.c"
4223void printMail(int msg )
4224{ int tmp ;
4225 int tmp___0 ;
4226 char const * __restrict __cil_tmp4 ;
4227 char const * __restrict __cil_tmp5 ;
4228
4229 {
4230 {
4231#line 18
4232 printMail__wrappee__Keys(msg);
4233#line 19
4234 tmp = isEncrypted(msg);
4235#line 19
4236 __cil_tmp4 = (char const * __restrict )"ENCRYPTED\n %d\n";
4237#line 19
4238 printf(__cil_tmp4, tmp);
4239#line 20
4240 tmp___0 = getEmailEncryptionKey(msg);
4241#line 20
4242 __cil_tmp5 = (char const * __restrict )"ENCRYPTION KEY\n %d\n";
4243#line 20
4244 printf(__cil_tmp5, tmp___0);
4245 }
4246#line 625 "Email.c"
4247 return;
4248}
4249}
4250#line 26 "Email.c"
4251int isReadable__wrappee__Keys(int msg )
4252{ int retValue_acc ;
4253
4254 {
4255#line 643 "Email.c"
4256 retValue_acc = 1;
4257#line 645
4258 return (retValue_acc);
4259#line 652
4260 return (retValue_acc);
4261}
4262}
4263#line 34 "Email.c"
4264int isReadable(int msg )
4265{ int retValue_acc ;
4266 int tmp ;
4267
4268 {
4269 {
4270#line 38
4271 tmp = isEncrypted(msg);
4272 }
4273#line 38 "Email.c"
4274 if (tmp) {
4275#line 681
4276 retValue_acc = 0;
4277#line 683
4278 return (retValue_acc);
4279 } else {
4280 {
4281#line 675 "Email.c"
4282 retValue_acc = isReadable__wrappee__Keys(msg);
4283 }
4284#line 677
4285 return (retValue_acc);
4286 }
4287#line 690 "Email.c"
4288 return (retValue_acc);
4289}
4290}
4291#line 42 "Email.c"
4292int cloneEmail(int msg )
4293{ int retValue_acc ;
4294
4295 {
4296#line 712 "Email.c"
4297 retValue_acc = msg;
4298#line 714
4299 return (retValue_acc);
4300#line 721
4301 return (retValue_acc);
4302}
4303}
4304#line 47 "Email.c"
4305int createEmail(int from , int to )
4306{ int retValue_acc ;
4307 int msg ;
4308
4309 {
4310 {
4311#line 48
4312 msg = 1;
4313#line 49
4314 setEmailFrom(msg, from);
4315#line 50
4316 setEmailTo(msg, to);
4317#line 751 "Email.c"
4318 retValue_acc = msg;
4319 }
4320#line 753
4321 return (retValue_acc);
4322#line 760
4323 return (retValue_acc);
4324}
4325}