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