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