Download Paper - STS

Appendix
19
20
21
22
|
|
|
|
23
24
25
26
27
28
29 (∗ ∗
|
|
|
|
|
30
31
32
33
34
35
36
37
38
Here we c h e c k i f i n t h e c u r r e n t s t a t e m e n t e i t h e r a
warning i s thrown , i n t h a t c a s e we add i t t o our l i s t o f
e x p r e s s i o n s , i f i t a new exp o t h e r w i s e we add i t t o t h e
redudandant warnings , or i f a v a r i a b l e o f any exp i s newly
a s s i g n e d i n t h a t c a s e we k i l l a l l e x p r e s s i o n s w i t h t h a t
v a r i a b l e . ∗)
l e t c a l c u l a t e n e x t f l o w d a t a l v a l exp ( f l o w v a l , warn , removes )
myWarnings s t m t =
l e t i s w a r n i n g = i s t h e r e c u r r e n t w a r n i n g myWarnings s t m t .
s i d in
l e t ( new flow , new warn , new removes ) = match i s w a r n i n g with
| f a l s e −> ( f l o w v a l , warn , removes )
| true when ( e x p e x i s t s i n f l o w d a t a f l o w v a l exp ) −> (
f l o w v a l , i n s e r t w a r n i n g warn ( g e t c u r r e n t c o d e a n n o t
myWarnings s t m t . s i d ) , removes )
| true when c h e c k f o r a n n o t s ( g e t c u r r e n t c o d e a n n o t
myWarnings s t m t . s i d ) warn −> ( C i l d a t a t y p e .
ExpStructEq . S e t . add exp f l o w v a l , warn , i n s e r t w a r n i n g
removes ( g e t c u r r e n t c o d e a n n o t myWarnings s t m t . s i d ) )
| true −> ( C i l d a t a t y p e . ExpStructEq . S e t . add exp f l o w v a l ,
warn , removes )
in
l e t k i l l s e t = c h e c k f o r l v a l ( C i l d a t a t y p e . ExpStructEq . S e t
. e l e m e n t s n e w f l o w ) l v a l in
( r e m o v e f l o w d a t a k i l l s e t new flow , new warn , new removes )
39
40
41 (∗ ∗
42
43
44
45
28
SizeOfE exp −> f i n d l v a l s exp
AlignOfE exp −> f i n d l v a l s exp
UnOp ( , exp , ) −> f i n d l v a l s exp
BinOp ( , exp1 , exp2 , ) −> f i n d l v a l s exp1 @
f i n d l v a l s exp2
CastE ( , exp ) −> f i n d l v a l s exp
AddrOf l v a l −> [ l v a l ]
S t a r t O f l v a l −> [ l v a l ]
I n f o ( exp , ) −> f i n d l v a l s exp
−> [ ]
returns true of for a given expression i t contains a
c e r t a i n v a r i a b l e . ∗)
l e t rec l v a l i s i n e x p exps l v a l = match exps with
| [ ] −> f a l s e
| x : : when C i l d a t a t y p e . L v a l S t r u c t E q . e q u a l x l v a l −> true
| ( , Index ( e , ) ) : : when l v a l i s i n e x p ( f i n d l v a l s e )
l v a l −> true