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