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