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