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