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