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