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