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