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