Information Technology Reference
In-Depth Information
V
C
:
f
FB
c
;
N
c
;
ZN
c
;
h1
c
;
h2
c
; rd :
FB
c
; wr:
N
c
g
C
:ZN
c
=1
^ pc
=
l
0
8
:
9
;
(h1
0
c
= T)
^
1))
^
(h2
0
c
)
(N
0
c
=FB
c
))
^
(
:
h2
0
c
)
(FB
0
c
=FB
c
^
N
c
=ZN
c
−
1))
^
(ZN
0
c
=N
c
)
^
(
rd :
FB
0
c
=h2
c
)
^
(
wr:
N
0
c
= T)
(h2
0
c
=(ZN
c
C
:
O
FB
:
if
rd
:
FB
c
then
FB
c
else
?
O
N
:
if
wr
:
N
c
then
N
c
else
?
Fig. 2.
Composite
sts
corresponding to the instrumented
C
program.
O
c
and removing their denition
denition of the instrumented variables into
from
C
. The actual implementation of the presented techniques within the code
validation tool CVT never explicitly generate the instrumented version of the
program but computes directly the simplied version as presented in Fig. 3.
V
C
:
f
FB
c
;
N
c
;
ZN
c
;
h1
c
;
h2
c
g
C
:ZN
c
=1
^ pc
=
l
0
:
;
(h1
0
c
= T)
^
(h2
0
c
=(ZN
c
1))
^
(h2
0
c
)
(N
0
c
=FB
c
))
^
(
:
h2
0
c
)
(FB
0
c
=FB
c
^
N
c
=ZN
c
−
1))
^
C
:
(ZN
0
c
=N
c
)
O
FB
:
if
h2
c
then
FB
c
else
?
O
N
:N
c
Fig. 3.
The actual (simplied)
sts
dec
as generated by the CVT tool.
Before computing the composite
corresponding to a given C program, the
CVT tool performs some syntactic checks. For example, it checks that all refer-
ences to an input variable
sts
i 2 I
syntactically succeed the statement which reads
the external input into
i
. Symmetrically, the tool checks that all assignments
to an output variable
o 2 O
syntactically precede the statement which exter-
nally writes
. Failure in any of these checks will cause the tool to declare the
translation as invalid.
o
Search WWH ::
Custom Search