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