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