A mixed modified axiomatic semantics of C-kernel language is described. This language is a kernel of C-light language oriented to verification. This semantics is a basement of verification conditions generator of C-kernel programs. Several examples which illustrate the use of inference rules are considered.