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