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