2021-01-15 15:55 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001922Frama-CPlug-in > wppublic2015-03-17 22:18
Reporterlapawczykt 
Assigned Tocorrenson 
PriorityurgentSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSxubuntuOS Version14.04
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001922: WP-Plugin crashes due to an internal error
DescriptionWhen the attached file is called with the command line, that reads as follows:

frama-c.byte -pp-annot -no-unicode -wp -wp-no-bits -wp-rte -wp-script 'wp0.script' -wp-model Typed+ref -wp-out foo.wp foo.c

Frama-C produces the following output:

[kernel] preprocessing with "gcc -C -E -I. -dD foo.c"
Adhesion_Factor.c:1:0: warning: "__STDC__" redefined [enabled by default]
 /* =============================================================================
 ^
foo.c:1:0: note: this is the location of the previous definition
 # 1 "Adhesion_Factor.c"
 ^
Adhesion_Factor.c:1:0: warning: "__STDC_HOSTED__" redefined [enabled by default]
 /* =============================================================================
 ^
foo.c:1:0: note: this is the location of the previous definition
 # 1 "Adhesion_Factor.c"
 ^
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function TrackToTrain_Packet_071
[rte] annotating function TrackToTrain_Packet_071_Encoder
[wp] Collecting variable usage
[wp] Computing [100 goals...]
[wp] failure: Non-assignable term (P_Telegram+(0 .. I_Cur_Dim-1))
[kernel] Current source was: Adhesion_Factor.c:59
         The full backtrace is:
         Raised at file "src/kernel/log.ml", line 524, characters 30-31
         Called from file "src/kernel/log.ml", line 518, characters 9-16
         Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
         Called from file "list.ml", line 55, characters 20-23
         Called from file "set.ml", line 304, characters 38-41
         Called from file "map.ml", line 168, characters 20-25
         Called from file "map.ml", line 168, characters 10-18
         Called from file "map.ml", line 168, characters 10-18
         Called from file "src/lib/bag.ml", line 96, characters 16-24
         Called from file "src/lib/bag.ml", line 96, characters 16-24
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 37, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
         
         Plug-in wp aborted: internal error.
         Please report as 'crash' at http://bts.frama-c.com/.
         Your Frama-C version is Neon-20140301.
         Note that a version and a backtrace alone often do not contain enough
         information to understand the bug. Guidelines for reporting bugs are at:
         http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
Additional InformationThe attached foo.c is the preprocessed version of a file out of the openETCS project. All used predicates are already included in the file.
TagsNo tags attached.
Attached Files
  • c file icon foo.c (97,160 bytes) 2014-09-12 15:34 -
    # 1 "Adhesion_Factor.c"
    #define __STDC__ 1
    # 1 "Adhesion_Factor.c"
    #define __STDC_HOSTED__ 1
    # 1 "Adhesion_Factor.c"
    #define __GNUC__ 4
    # 1 "Adhesion_Factor.c"
    #define __GNUC_MINOR__ 8
    # 1 "Adhesion_Factor.c"
    #define __GNUC_PATCHLEVEL__ 2
    # 1 "Adhesion_Factor.c"
    #define __VERSION__ "4.8.2"
    # 1 "Adhesion_Factor.c"
    #define __ATOMIC_RELAXED 0
    # 1 "Adhesion_Factor.c"
    #define __ATOMIC_SEQ_CST 5
    # 1 "Adhesion_Factor.c"
    #define __ATOMIC_ACQUIRE 2
    # 1 "Adhesion_Factor.c"
    #define __ATOMIC_RELEASE 3
    # 1 "Adhesion_Factor.c"
    #define __ATOMIC_ACQ_REL 4
    # 1 "Adhesion_Factor.c"
    #define __ATOMIC_CONSUME 1
    # 1 "Adhesion_Factor.c"
    #define __FINITE_MATH_ONLY__ 0
    # 1 "Adhesion_Factor.c"
    #define _LP64 1
    # 1 "Adhesion_Factor.c"
    #define __LP64__ 1
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_INT__ 4
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_LONG__ 8
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_LONG_LONG__ 8
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_SHORT__ 2
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_FLOAT__ 4
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_DOUBLE__ 8
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_LONG_DOUBLE__ 16
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_SIZE_T__ 8
    # 1 "Adhesion_Factor.c"
    #define __CHAR_BIT__ 8
    # 1 "Adhesion_Factor.c"
    #define __BIGGEST_ALIGNMENT__ 16
    # 1 "Adhesion_Factor.c"
    #define __ORDER_LITTLE_ENDIAN__ 1234
    # 1 "Adhesion_Factor.c"
    #define __ORDER_BIG_ENDIAN__ 4321
    # 1 "Adhesion_Factor.c"
    #define __ORDER_PDP_ENDIAN__ 3412
    # 1 "Adhesion_Factor.c"
    #define __BYTE_ORDER__ __ORDER_LITTLE_ENDIAN__
    # 1 "Adhesion_Factor.c"
    #define __FLOAT_WORD_ORDER__ __ORDER_LITTLE_ENDIAN__
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_POINTER__ 8
    # 1 "Adhesion_Factor.c"
    #define __SIZE_TYPE__ long unsigned int
    # 1 "Adhesion_Factor.c"
    #define __PTRDIFF_TYPE__ long int
    # 1 "Adhesion_Factor.c"
    #define __WCHAR_TYPE__ int
    # 1 "Adhesion_Factor.c"
    #define __WINT_TYPE__ unsigned int
    # 1 "Adhesion_Factor.c"
    #define __INTMAX_TYPE__ long int
    # 1 "Adhesion_Factor.c"
    #define __UINTMAX_TYPE__ long unsigned int
    # 1 "Adhesion_Factor.c"
    #define __CHAR16_TYPE__ short unsigned int
    # 1 "Adhesion_Factor.c"
    #define __CHAR32_TYPE__ unsigned int
    # 1 "Adhesion_Factor.c"
    #define __SIG_ATOMIC_TYPE__ int
    # 1 "Adhesion_Factor.c"
    #define __INT8_TYPE__ signed char
    # 1 "Adhesion_Factor.c"
    #define __INT16_TYPE__ short int
    # 1 "Adhesion_Factor.c"
    #define __INT32_TYPE__ int
    # 1 "Adhesion_Factor.c"
    #define __INT64_TYPE__ long int
    # 1 "Adhesion_Factor.c"
    #define __UINT8_TYPE__ unsigned char
    # 1 "Adhesion_Factor.c"
    #define __UINT16_TYPE__ short unsigned int
    # 1 "Adhesion_Factor.c"
    #define __UINT32_TYPE__ unsigned int
    # 1 "Adhesion_Factor.c"
    #define __UINT64_TYPE__ long unsigned int
    # 1 "Adhesion_Factor.c"
    #define __INT_LEAST8_TYPE__ signed char
    # 1 "Adhesion_Factor.c"
    #define __INT_LEAST16_TYPE__ short int
    # 1 "Adhesion_Factor.c"
    #define __INT_LEAST32_TYPE__ int
    # 1 "Adhesion_Factor.c"
    #define __INT_LEAST64_TYPE__ long int
    # 1 "Adhesion_Factor.c"
    #define __UINT_LEAST8_TYPE__ unsigned char
    # 1 "Adhesion_Factor.c"
    #define __UINT_LEAST16_TYPE__ short unsigned int
    # 1 "Adhesion_Factor.c"
    #define __UINT_LEAST32_TYPE__ unsigned int
    # 1 "Adhesion_Factor.c"
    #define __UINT_LEAST64_TYPE__ long unsigned int
    # 1 "Adhesion_Factor.c"
    #define __INT_FAST8_TYPE__ signed char
    # 1 "Adhesion_Factor.c"
    #define __INT_FAST16_TYPE__ long int
    # 1 "Adhesion_Factor.c"
    #define __INT_FAST32_TYPE__ long int
    # 1 "Adhesion_Factor.c"
    #define __INT_FAST64_TYPE__ long int
    # 1 "Adhesion_Factor.c"
    #define __UINT_FAST8_TYPE__ unsigned char
    # 1 "Adhesion_Factor.c"
    #define __UINT_FAST16_TYPE__ long unsigned int
    # 1 "Adhesion_Factor.c"
    #define __UINT_FAST32_TYPE__ long unsigned int
    # 1 "Adhesion_Factor.c"
    #define __UINT_FAST64_TYPE__ long unsigned int
    # 1 "Adhesion_Factor.c"
    #define __INTPTR_TYPE__ long int
    # 1 "Adhesion_Factor.c"
    #define __UINTPTR_TYPE__ long unsigned int
    # 1 "Adhesion_Factor.c"
    #define __GXX_ABI_VERSION 1002
    # 1 "Adhesion_Factor.c"
    #define __SCHAR_MAX__ 127
    # 1 "Adhesion_Factor.c"
    #define __SHRT_MAX__ 32767
    # 1 "Adhesion_Factor.c"
    #define __INT_MAX__ 2147483647
    # 1 "Adhesion_Factor.c"
    #define __LONG_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __LONG_LONG_MAX__ 9223372036854775807LL
    # 1 "Adhesion_Factor.c"
    #define __WCHAR_MAX__ 2147483647
    # 1 "Adhesion_Factor.c"
    #define __WCHAR_MIN__ (-__WCHAR_MAX__ - 1)
    # 1 "Adhesion_Factor.c"
    #define __WINT_MAX__ 4294967295U
    # 1 "Adhesion_Factor.c"
    #define __WINT_MIN__ 0U
    # 1 "Adhesion_Factor.c"
    #define __PTRDIFF_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __SIZE_MAX__ 18446744073709551615UL
    # 1 "Adhesion_Factor.c"
    #define __INTMAX_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __INTMAX_C(c) c ## L
    # 1 "Adhesion_Factor.c"
    #define __UINTMAX_MAX__ 18446744073709551615UL
    # 1 "Adhesion_Factor.c"
    #define __UINTMAX_C(c) c ## UL
    # 1 "Adhesion_Factor.c"
    #define __SIG_ATOMIC_MAX__ 2147483647
    # 1 "Adhesion_Factor.c"
    #define __SIG_ATOMIC_MIN__ (-__SIG_ATOMIC_MAX__ - 1)
    # 1 "Adhesion_Factor.c"
    #define __INT8_MAX__ 127
    # 1 "Adhesion_Factor.c"
    #define __INT16_MAX__ 32767
    # 1 "Adhesion_Factor.c"
    #define __INT32_MAX__ 2147483647
    # 1 "Adhesion_Factor.c"
    #define __INT64_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __UINT8_MAX__ 255
    # 1 "Adhesion_Factor.c"
    #define __UINT16_MAX__ 65535
    # 1 "Adhesion_Factor.c"
    #define __UINT32_MAX__ 4294967295U
    # 1 "Adhesion_Factor.c"
    #define __UINT64_MAX__ 18446744073709551615UL
    # 1 "Adhesion_Factor.c"
    #define __INT_LEAST8_MAX__ 127
    # 1 "Adhesion_Factor.c"
    #define __INT8_C(c) c
    # 1 "Adhesion_Factor.c"
    #define __INT_LEAST16_MAX__ 32767
    # 1 "Adhesion_Factor.c"
    #define __INT16_C(c) c
    # 1 "Adhesion_Factor.c"
    #define __INT_LEAST32_MAX__ 2147483647
    # 1 "Adhesion_Factor.c"
    #define __INT32_C(c) c
    # 1 "Adhesion_Factor.c"
    #define __INT_LEAST64_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __INT64_C(c) c ## L
    # 1 "Adhesion_Factor.c"
    #define __UINT_LEAST8_MAX__ 255
    # 1 "Adhesion_Factor.c"
    #define __UINT8_C(c) c
    # 1 "Adhesion_Factor.c"
    #define __UINT_LEAST16_MAX__ 65535
    # 1 "Adhesion_Factor.c"
    #define __UINT16_C(c) c
    # 1 "Adhesion_Factor.c"
    #define __UINT_LEAST32_MAX__ 4294967295U
    # 1 "Adhesion_Factor.c"
    #define __UINT32_C(c) c ## U
    # 1 "Adhesion_Factor.c"
    #define __UINT_LEAST64_MAX__ 18446744073709551615UL
    # 1 "Adhesion_Factor.c"
    #define __UINT64_C(c) c ## UL
    # 1 "Adhesion_Factor.c"
    #define __INT_FAST8_MAX__ 127
    # 1 "Adhesion_Factor.c"
    #define __INT_FAST16_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __INT_FAST32_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __INT_FAST64_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __UINT_FAST8_MAX__ 255
    # 1 "Adhesion_Factor.c"
    #define __UINT_FAST16_MAX__ 18446744073709551615UL
    # 1 "Adhesion_Factor.c"
    #define __UINT_FAST32_MAX__ 18446744073709551615UL
    # 1 "Adhesion_Factor.c"
    #define __UINT_FAST64_MAX__ 18446744073709551615UL
    # 1 "Adhesion_Factor.c"
    #define __INTPTR_MAX__ 9223372036854775807L
    # 1 "Adhesion_Factor.c"
    #define __UINTPTR_MAX__ 18446744073709551615UL
    # 1 "Adhesion_Factor.c"
    #define __FLT_EVAL_METHOD__ 0
    # 1 "Adhesion_Factor.c"
    #define __DEC_EVAL_METHOD__ 2
    # 1 "Adhesion_Factor.c"
    #define __FLT_RADIX__ 2
    # 1 "Adhesion_Factor.c"
    #define __FLT_MANT_DIG__ 24
    # 1 "Adhesion_Factor.c"
    #define __FLT_DIG__ 6
    # 1 "Adhesion_Factor.c"
    #define __FLT_MIN_EXP__ (-125)
    # 1 "Adhesion_Factor.c"
    #define __FLT_MIN_10_EXP__ (-37)
    # 1 "Adhesion_Factor.c"
    #define __FLT_MAX_EXP__ 128
    # 1 "Adhesion_Factor.c"
    #define __FLT_MAX_10_EXP__ 38
    # 1 "Adhesion_Factor.c"
    #define __FLT_DECIMAL_DIG__ 9
    # 1 "Adhesion_Factor.c"
    #define __FLT_MAX__ 3.40282346638528859812e+38F
    # 1 "Adhesion_Factor.c"
    #define __FLT_MIN__ 1.17549435082228750797e-38F
    # 1 "Adhesion_Factor.c"
    #define __FLT_EPSILON__ 1.19209289550781250000e-7F
    # 1 "Adhesion_Factor.c"
    #define __FLT_DENORM_MIN__ 1.40129846432481707092e-45F
    # 1 "Adhesion_Factor.c"
    #define __FLT_HAS_DENORM__ 1
    # 1 "Adhesion_Factor.c"
    #define __FLT_HAS_INFINITY__ 1
    # 1 "Adhesion_Factor.c"
    #define __FLT_HAS_QUIET_NAN__ 1
    # 1 "Adhesion_Factor.c"
    #define __DBL_MANT_DIG__ 53
    # 1 "Adhesion_Factor.c"
    #define __DBL_DIG__ 15
    # 1 "Adhesion_Factor.c"
    #define __DBL_MIN_EXP__ (-1021)
    # 1 "Adhesion_Factor.c"
    #define __DBL_MIN_10_EXP__ (-307)
    # 1 "Adhesion_Factor.c"
    #define __DBL_MAX_EXP__ 1024
    # 1 "Adhesion_Factor.c"
    #define __DBL_MAX_10_EXP__ 308
    # 1 "Adhesion_Factor.c"
    #define __DBL_DECIMAL_DIG__ 17
    # 1 "Adhesion_Factor.c"
    #define __DBL_MAX__ ((double)1.79769313486231570815e+308L)
    # 1 "Adhesion_Factor.c"
    #define __DBL_MIN__ ((double)2.22507385850720138309e-308L)
    # 1 "Adhesion_Factor.c"
    #define __DBL_EPSILON__ ((double)2.22044604925031308085e-16L)
    # 1 "Adhesion_Factor.c"
    #define __DBL_DENORM_MIN__ ((double)4.94065645841246544177e-324L)
    # 1 "Adhesion_Factor.c"
    #define __DBL_HAS_DENORM__ 1
    # 1 "Adhesion_Factor.c"
    #define __DBL_HAS_INFINITY__ 1
    # 1 "Adhesion_Factor.c"
    #define __DBL_HAS_QUIET_NAN__ 1
    # 1 "Adhesion_Factor.c"
    #define __LDBL_MANT_DIG__ 64
    # 1 "Adhesion_Factor.c"
    #define __LDBL_DIG__ 18
    # 1 "Adhesion_Factor.c"
    #define __LDBL_MIN_EXP__ (-16381)
    # 1 "Adhesion_Factor.c"
    #define __LDBL_MIN_10_EXP__ (-4931)
    # 1 "Adhesion_Factor.c"
    #define __LDBL_MAX_EXP__ 16384
    # 1 "Adhesion_Factor.c"
    #define __LDBL_MAX_10_EXP__ 4932
    # 1 "Adhesion_Factor.c"
    #define __DECIMAL_DIG__ 21
    # 1 "Adhesion_Factor.c"
    #define __LDBL_MAX__ 1.18973149535723176502e+4932L
    # 1 "Adhesion_Factor.c"
    #define __LDBL_MIN__ 3.36210314311209350626e-4932L
    # 1 "Adhesion_Factor.c"
    #define __LDBL_EPSILON__ 1.08420217248550443401e-19L
    # 1 "Adhesion_Factor.c"
    #define __LDBL_DENORM_MIN__ 3.64519953188247460253e-4951L
    # 1 "Adhesion_Factor.c"
    #define __LDBL_HAS_DENORM__ 1
    # 1 "Adhesion_Factor.c"
    #define __LDBL_HAS_INFINITY__ 1
    # 1 "Adhesion_Factor.c"
    #define __LDBL_HAS_QUIET_NAN__ 1
    # 1 "Adhesion_Factor.c"
    #define __DEC32_MANT_DIG__ 7
    # 1 "Adhesion_Factor.c"
    #define __DEC32_MIN_EXP__ (-94)
    # 1 "Adhesion_Factor.c"
    #define __DEC32_MAX_EXP__ 97
    # 1 "Adhesion_Factor.c"
    #define __DEC32_MIN__ 1E-95DF
    # 1 "Adhesion_Factor.c"
    #define __DEC32_MAX__ 9.999999E96DF
    # 1 "Adhesion_Factor.c"
    #define __DEC32_EPSILON__ 1E-6DF
    # 1 "Adhesion_Factor.c"
    #define __DEC32_SUBNORMAL_MIN__ 0.000001E-95DF
    # 1 "Adhesion_Factor.c"
    #define __DEC64_MANT_DIG__ 16
    # 1 "Adhesion_Factor.c"
    #define __DEC64_MIN_EXP__ (-382)
    # 1 "Adhesion_Factor.c"
    #define __DEC64_MAX_EXP__ 385
    # 1 "Adhesion_Factor.c"
    #define __DEC64_MIN__ 1E-383DD
    # 1 "Adhesion_Factor.c"
    #define __DEC64_MAX__ 9.999999999999999E384DD
    # 1 "Adhesion_Factor.c"
    #define __DEC64_EPSILON__ 1E-15DD
    # 1 "Adhesion_Factor.c"
    #define __DEC64_SUBNORMAL_MIN__ 0.000000000000001E-383DD
    # 1 "Adhesion_Factor.c"
    #define __DEC128_MANT_DIG__ 34
    # 1 "Adhesion_Factor.c"
    #define __DEC128_MIN_EXP__ (-6142)
    # 1 "Adhesion_Factor.c"
    #define __DEC128_MAX_EXP__ 6145
    # 1 "Adhesion_Factor.c"
    #define __DEC128_MIN__ 1E-6143DL
    # 1 "Adhesion_Factor.c"
    #define __DEC128_MAX__ 9.999999999999999999999999999999999E6144DL
    # 1 "Adhesion_Factor.c"
    #define __DEC128_EPSILON__ 1E-33DL
    # 1 "Adhesion_Factor.c"
    #define __DEC128_SUBNORMAL_MIN__ 0.000000000000000000000000000000001E-6143DL
    # 1 "Adhesion_Factor.c"
    #define __REGISTER_PREFIX__
    # 1 "Adhesion_Factor.c"
    #define __USER_LABEL_PREFIX__
    # 1 "Adhesion_Factor.c"
    #define __GNUC_GNU_INLINE__ 1
    # 1 "Adhesion_Factor.c"
    #define __NO_INLINE__ 1
    # 1 "Adhesion_Factor.c"
    #define __GCC_HAVE_SYNC_COMPARE_AND_SWAP_1 1
    # 1 "Adhesion_Factor.c"
    #define __GCC_HAVE_SYNC_COMPARE_AND_SWAP_2 1
    # 1 "Adhesion_Factor.c"
    #define __GCC_HAVE_SYNC_COMPARE_AND_SWAP_4 1
    # 1 "Adhesion_Factor.c"
    #define __GCC_HAVE_SYNC_COMPARE_AND_SWAP_8 1
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_BOOL_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_CHAR_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_CHAR16_T_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_CHAR32_T_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_WCHAR_T_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_SHORT_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_INT_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_LONG_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_LLONG_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_TEST_AND_SET_TRUEVAL 1
    # 1 "Adhesion_Factor.c"
    #define __GCC_ATOMIC_POINTER_LOCK_FREE 2
    # 1 "Adhesion_Factor.c"
    #define __GCC_HAVE_DWARF2_CFI_ASM 1
    # 1 "Adhesion_Factor.c"
    #define __PRAGMA_REDEFINE_EXTNAME 1
    # 1 "Adhesion_Factor.c"
    #define __SSP__ 1
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_INT128__ 16
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_WCHAR_T__ 4
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_WINT_T__ 4
    # 1 "Adhesion_Factor.c"
    #define __SIZEOF_PTRDIFF_T__ 8
    # 1 "Adhesion_Factor.c"
    #define __amd64 1
    # 1 "Adhesion_Factor.c"
    #define __amd64__ 1
    # 1 "Adhesion_Factor.c"
    #define __x86_64 1
    # 1 "Adhesion_Factor.c"
    #define __x86_64__ 1
    # 1 "Adhesion_Factor.c"
    #define __ATOMIC_HLE_ACQUIRE 65536
    # 1 "Adhesion_Factor.c"
    #define __ATOMIC_HLE_RELEASE 131072
    # 1 "Adhesion_Factor.c"
    #define __k8 1
    # 1 "Adhesion_Factor.c"
    #define __k8__ 1
    # 1 "Adhesion_Factor.c"
    #define __code_model_small__ 1
    # 1 "Adhesion_Factor.c"
    #define __MMX__ 1
    # 1 "Adhesion_Factor.c"
    #define __SSE__ 1
    # 1 "Adhesion_Factor.c"
    #define __SSE2__ 1
    # 1 "Adhesion_Factor.c"
    #define __FXSR__ 1
    # 1 "Adhesion_Factor.c"
    #define __SSE_MATH__ 1
    # 1 "Adhesion_Factor.c"
    #define __SSE2_MATH__ 1
    # 1 "Adhesion_Factor.c"
    #define __gnu_linux__ 1
    # 1 "Adhesion_Factor.c"
    #define __linux 1
    # 1 "Adhesion_Factor.c"
    #define __linux__ 1
    # 1 "Adhesion_Factor.c"
    #define linux 1
    # 1 "Adhesion_Factor.c"
    #define __unix 1
    # 1 "Adhesion_Factor.c"
    #define __unix__ 1
    # 1 "Adhesion_Factor.c"
    #define unix 1
    # 1 "Adhesion_Factor.c"
    #define __ELF__ 1
    # 1 "Adhesion_Factor.c"
    #define __DECIMAL_BID_FORMAT__ 1
    # 1 "<command-line>"
    # 1 "Adhesion_Factor.c"
    /* =============================================================================
     Formalization of Subset-026-7 (Chapter 7: ERTMS/ETCS language)
     
     - Name: Subset-026-7 / Adhesion_Factor
     - Description: UNISIG SUBSET-026-7, ISSUE : 3.3.0, 3.5 ERTMS/ETCS language)
     - Copyright (c) Siemens AG, CPYRGHT, All Rights Reserved
     
     - Licensed under the EUPL V.1.1 ( http://joinup.ec.europa.eu/software/page/eupl/licence-eupl )
     - Gist URL: none
     - Cryptography: No
     - Author(s): SiemensRailAutomation
     
     Disclaimer:
     
     The use of this software is limited to NON-vital applications.
     It has NOT been developed for vital operation purposes and MUST NOT be used for applications
     which may cause harm to people, physical accidents or financial loss.
     
     THEREFORE, NO LIABILITY WILL BE GIVEN FOR SUCH AND ANY OTHER KIND OF USE.
     ============================================================================= */
    # 1 "Adhesion_Factor.h" 1
    
    #define NESTINGMARK_oETCS_Packet_TrackToTrain_Adhesion_Factor
    /* =============================================================================
     Formalization of Subset-026-7 (Chapter 7: ERTMS/ETCS language)
     
     - Name: Subset-026-7 / TrackToTrain_Adhesion_Factor
     - Description: UNISIG SUBSET-026-7, ISSUE : 3.3.0, 3.5 ERTMS/ETCS language)
     - Copyright (c) Siemens AG, 2014, All Rights Reserved
     
     - Licensed under the EUPL V.1.1 ( http://joinup.ec.europa.eu/software/page/eupl/licence-eupl )
     - Gist URL: none
     - Cryptography: No
     - Author(s): SiemensRailAutomation
     
     Disclaimer:
     
     The use of this software is limited to NON-vital applications.
     It has NOT been developed for vital operation purposes and MUST NOT be used for applications
     which may cause harm to people, physical accidents or financial loss.
     
     THEREFORE, NO LIABILITY WILL BE GIVEN FOR SUCH AND ANY OTHER KIND OF USE.
     ============================================================================= */
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 1
    
    #define BITWALKER_H
    
    # 1 "/usr/local/share/frama-c/libc/stdint.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    /* ISO C: 7.18 */
    
    #define __FC_STDINT
    # 1 "/usr/local/share/frama-c/libc/__fc_machdep.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    
    #define __FC_MACHDEP
    
    
    
    #define __FC_MACHDEP_X86_32
    
    
    
    
    #define __FC_FORCE_INCLUDE_MACHDEP__
    # 1 "/usr/local/share/frama-c/libc/__fc_machdep_linux_gcc_shared.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    
    
    
    /* This file contains common machine specific values between
     Linux/GCC x86 32-bit, AMD64 and x86 16-bit.*/
    
    
    #define __FC_MACHDEP_LINUX_SHARED
    
    /* Optional */
    #define __INT8_T signed char
    #define __UINT8_T unsigned char
    #define __INT16_T signed short
    #define __UINT16_T unsigned short
    
    /* Required */
    #define __INT_LEAST8_T signed char
    #define __UINT_LEAST8_T unsigned char
    #define __INT_LEAST16_T signed short
    #define __UINT_LEAST16_T unsigned short
    #define __INT_LEAST64_T signed long long
    #define __UINT_LEAST64_T unsigned long long
    
    /* Required */
    #define __INT_FAST8_T signed char
    #define __UINT_FAST8_T unsigned char
    #define __INT_FAST16_T signed int
    #define __UINT_FAST16_T unsigned int
    #define __INT_FAST64_T signed long long
    #define __UINT_FAST64_T unsigned long long
    
    /* Required */
    #define __INT_MAX_T signed long long
    #define __UINT_MAX_T unsigned long long
    
    /* min and max values as specified in limits.h */
    #define __FC_SCHAR_MIN (-128)
    #define __FC_SCHAR_MAX 127
    #define __FC_UCHAR_MAX 255
    #define __FC_SHRT_MIN (-32768)
    #define __FC_SHRT_MAX 32767
    #define __FC_USHRT_MAX 65535
    #define __FC_INT_MIN (-INT_MAX - 1)
    #define __FC_INT_MAX 2147483647
    #define __FC_UINT_MAX 4294967295U
    #define __FC_LONG_MIN (-LONG_MAX -1L)
    #define __FC_LLONG_MIN (-LLONG_MAX -1LL)
    #define __FC_LLONG_MAX 9223372036854775807LL
    #define __FC_ULLONG_MAX 18446744073709551615ULL
    
    /* Unused at this time */
    #define __FC_umax(n) ((uint ##n ##_t)(-1))
    #define __FC_smin(n) (2*(-(1ll << (sizeof(int ##n ##_t)*__CHAR_BIT - 2))))
    #define __FC_smax(n) ((1ll<<(sizeof(int ##n ##_t)*__CHAR_BIT - 2))-1+(1ll<<(sizeof(int ##n ##_t)*__CHAR_BIT - 2)))
    
    /* stdint.h */
    /* NB: in signal.h, sig_atomic_t is hardwired to int. */
    #define __FC_SIG_ATOMIC_MIN __FC_INT_MIN
    #define __FC_SIG_ATOMIC_MAX __FC_INT_MAX
    #define __FC_SIZE_MAX __FC_UINT_MAX
    #define __FC_WCHAR_MIN __FC_INT_MIN
    #define __FC_WCHAR_MAX __FC_INT_MAX
    
    // To be defined in coordination with wchar.h which is currently unsupported
    #define __WCHAR_T int
    #define __FC_WINT_MIN __FC_INT_MIN
    #define __FC_WINT_MAX __FC_INT_MAX
    // 7.25 mandates that WINT_T can handle at least one character in addition
    // to those that are in the extended character set (to account for EOF)
    #define __WINT_T long long int
    
    /* stdio.h */
    #define __FC_BUFSIZ 8192
    #define __FC_EOF (-1)
    #define __FC_FOPEN_MAX 512
    #define __FC_FILENAME_MAX 2048
    #define __FC_L_tmpnam 2048
    #define __FC_TMP_MAX 0xFFFFFFFF
    
    /* stdlib.h */
    #define __FC_RAND_MAX 32767
    #define __FC_MB_CUR_MAX ((size_t)16)
    
    /* errno.h */
    #define __FC_EDOM 1
    #define __FC_EILSEQ 2
    #define __FC_ERANGE 3
    
    #define __FC_E2BIG 4
    #define __FC_EACCES 5
    #define __FC_EADDRINUSE 6
    #define __FC_EADDRNOTAVAIL 7
    #define __FC_EAFNOSUPPORT 8
    #define __FC_EAGAIN 9
    #define __FC_EALREADY 10
    #define __FC_EBADE 11
    #define __FC_EBADF 12
    #define __FC_EBADFD 13
    #define __FC_EBADMSG 14
    #define __FC_EBADR 15
    #define __FC_EBADRQC 16
    #define __FC_EBADSLT 17
    #define __FC_EBUSY 18
    #define __FC_ECANCELED 19
    #define __FC_ECHILD 20
    #define __FC_ECHRNG 21
    #define __FC_ECOMM 22
    #define __FC_ECONNABORTED 23
    #define __FC_ECONNREFUSED 24
    #define __FC_ECONNRESET 25
    #define __FC_EDEADLK 26
    #define __FC_EDEADLOCK 27
    #define __FC_EDESTADDRREQ 28
    #define __FC_EDQUOT 29
    #define __FC_EEXIST 30
    #define __FC_EFAULT 31
    #define __FC_EFBIG 32
    #define __FC_EHOSTDOWN 33
    #define __FC_EHOSTUNREACH 34
    #define __FC_EIDRM 35
    #define __FC_EINPROGRESS 36
    #define __FC_EINTR 37
    #define __FC_EINVAL 38
    #define __FC_EIO 39
    #define __FC_EISCONN 40
    #define __FC_EISDIR 41
    #define __FC_EISNAM 42
    #define __FC_EKEYEXPIRED 43
    #define __FC_EKEYREJECTED 44
    #define __FC_EKEYREVOKED 45
    #define __FC_EL2HLT 46
    #define __FC_EL2NSYNC 47
    #define __FC_EL3HLT 48
    #define __FC_EL3RST 49
    #define __FC_ELIBACC 50
    #define __FC_ELIBBAD 51
    #define __FC_ELIBMAX 52
    #define __FC_ELIBSCN 53
    #define __FC_ELIBEXEC 54
    #define __FC_ELOOP 55
    #define __FC_EMEDIUMTYPE 56
    #define __FC_EMFILE 57
    #define __FC_EMLINK 58
    #define __FC_EMSGSIZE 59
    #define __FC_EMULTIHOP 60
    #define __FC_ENAMETOOLONG 61
    #define __FC_ENETDOWN 62
    #define __FC_ENETRESET 63
    #define __FC_ENETUNREACH 64
    #define __FC_ENFILE 65
    #define __FC_ENOBUFS 66
    #define __FC_ENODATA 67
    #define __FC_ENODEV 68
    #define __FC_ENOENT 69
    #define __FC_ENOEXEC 70
    #define __FC_ENOKEY 71
    #define __FC_ENOLCK 72
    #define __FC_ENOLINK 73
    #define __FC_ENOMEDIUM 74
    #define __FC_ENOMEM 75
    #define __FC_ENOMSG 76
    #define __FC_ENONET 77
    #define __FC_ENOPKG 78
    #define __FC_ENOPROTOOPT 79
    #define __FC_ENOSPC 80
    #define __FC_ENOSR 81
    #define __FC_ENOSTR 82
    #define __FC_ENOSYS 83
    #define __FC_ENOTBLK 84
    #define __FC_ENOTCONN 85
    #define __FC_ENOTDIR 86
    #define __FC_ENOTEMPTY 87
    #define __FC_ENOTSOCK 88
    #define __FC_ENOTSUP 89
    #define __FC_ENOTTY 90
    #define __FC_ENOTUNIQ 91
    #define __FC_ENXIO 92
    #define __FC_EOPNOTSUPP 93
    #define __FC_EOVERFLOW 94
    #define __FC_EPERM 95
    #define __FC_EPFNOSUPPORT 96
    #define __FC_EPIPE 97
    #define __FC_EPROTO 98
    #define __FC_EPROTONOSUPPORT 99
    #define __FC_EPROTOTYPE 100
    #define __FC_EREMCHG 101
    #define __FC_EREMOTE 102
    #define __FC_EREMOTEIO 103
    #define __FC_ERESTART 104
    #define __FC_EROFS 105
    #define __FC_ESHUTDOWN 106
    #define __FC_ESPIPE 107
    #define __FC_ESOCKTNOSUPPORT 108
    #define __FC_ESRCH 109
    #define __FC_ESTALE 110
    #define __FC_ESTRPIPE 111
    #define __FC_ETIME 112
    #define __FC_ETIMEDOUT 113
    #define __FC_ETXTBSY 114
    #define __FC_EUCLEAN 115
    #define __FC_EUNATCH 116
    #define __FC_EUSERS 117
    #define __FC_EWOULDBLOCK 118
    #define __FC_EXDEV 119
    #define __FC_EXFULL 120
    
    /* sys/un.h */
    #define __FC_SOCKADDR_SUN_SUN_PATH 108
    # 35 "/usr/local/share/frama-c/libc/__fc_machdep.h" 2
    #undef __FC_FORCE_INCLUDE_MACHDEP__
    #define __FC_BYTE_ORDER __LITTLE_ENDIAN
    /* Required */
    #undef __CHAR_UNSIGNED__
    #define __WORDSIZE 32
    #define __SIZEOF_SHORT 2
    #define __SIZEOF_INT 4
    #define __SIZEOF_LONG 4
    #define __SIZEOF_LONGLONG 8
    #define __CHAR_BIT 8
    #define __SIZE_T unsigned int
    #define __PTRDIFF_T int
    #define __FC_LONG_MAX 2147483647L
    #define __FC_ULONG_MAX 4294967295UL
    
    /* Optional */
    #define __INTPTR_T signed int
    #define __UINTPTR_T unsigned int
    #define __INT32_T signed int
    #define __UINT32_T unsigned int
    #define __INT64_T signed long long
    #define __UINT64_T unsigned long long
    
    /* Required */
    #define __INT_LEAST32_T signed int
    #define __UINT_LEAST32_T unsigned int
    #define __INT_FAST32_T signed int
    #define __UINT_FAST32_T unsigned int
    
    /* POSIX */
    #define __SSIZE_T int
    /* stdint.h */
    #define __FC_PTRDIFF_MIN __FC_INT_MIN
    #define __FC_PTRDIFF_MAX __FC_INT_MAX
    # 27 "/usr/local/share/frama-c/libc/stdint.h" 2
    
    /* ISO C: 7.18.1.1 */
    
    typedef signed char int8_t;
    
    
    typedef unsigned char uint8_t;
    
    
    typedef signed short int16_t;
    
    
    typedef unsigned short uint16_t;
    
    
    typedef signed int int32_t;
    
    
    typedef unsigned int uint32_t;
    
    
    typedef signed long long int64_t;
    
    
    typedef unsigned long long uint64_t;
    
    
    /* ISO C: 7.18.1.2 */
    typedef signed char int_least8_t;
    typedef unsigned char uint_least8_t;
    typedef signed short int_least16_t;
    typedef unsigned short uint_least16_t;
    typedef signed int int_least32_t;
    typedef unsigned int uint_least32_t;
    typedef signed long long int_least64_t;
    typedef unsigned long long uint_least64_t;
    
    /* ISO C: 7.18.1.3 */
    typedef signed char int_fast8_t;
    typedef unsigned char uint_fast8_t;
    typedef signed int int_fast16_t;
    typedef unsigned int uint_fast16_t;
    typedef signed int int_fast32_t;
    typedef unsigned int uint_fast32_t;
    typedef signed long long int_fast64_t;
    typedef unsigned long long uint_fast64_t;
    
    /* ISO C: 7.18.1.4 */
    # 1 "/usr/local/share/frama-c/libc/__fc_define_intptr_t.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    
    #define __FC_DEFINE_INTPTR_T
    # 1 "/usr/local/share/frama-c/libc/__fc_machdep.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    # 26 "/usr/local/share/frama-c/libc/__fc_define_intptr_t.h" 2
    
    
    typedef signed int intptr_t;
    # 76 "/usr/local/share/frama-c/libc/stdint.h" 2
    
    
    typedef unsigned int uintptr_t;
    
    
    /* ISO C: 7.18.1.5 */
    typedef signed long long intmax_t;
    typedef unsigned long long uintmax_t;
    
    /* ISO C: 7.18.2.1 */
    #define INT8_MIN (-128)
    #define INT8_MAX 127
    #define UINT8_MAX 255
    #define INT16_MIN (-32768)
    #define INT16_MAX 32767
    #define UINT16_MAX 65535
    #define INT32_MIN (-INT32_MAX - 1)
    #define INT32_MAX 2147483647
    #define UINT32_MAX 4294967295U
    #define INT64_MIN (-INT64_MAX -1LL)
    #define INT64_MAX 9223372036854775807LL
    #define UINT64_MAX 18446744073709551615ULL
    
    /* ISO C: 7.18.2.3-5 : TODO */
    
    /* ISO C: 7.18.3 */
    
    #define PTRDIFF_MIN __FC_PTRDIFF_MIN
    #define PTRDIFF_MAX __FC_PTRDIFF_MAX
    #define SIG_ATOMIC_MIN __FC_SIG_ATOMIC_MIN
    #define SIG_ATOMIC_MAX __FC_SIG_ATOMIC_MAX
    #define SIZE_MAX __FC_SIZE_MAX
    #define WCHAR_MIN __FC_WCHAR_MIN
    #define WCHAR_MAX __FC_WCHAR_MAX
    #define WINT_MIN __FC_WINT_MIN
    #define WINT_MAX __FC_WINT_MAX
    
    /* ISO C: 7.18.4 */
    #define INT8_C(c) c
    #define UINT8_C(c) c
    #define INT16_C(c) c
    #define UINT16_C(c) c
    #define INT32_C(c) (c ## L)
    #define UINT32_C(c) (c ## UL)
    #define INT64_C(c) (c ## LL)
    #define UINT64_C(c) (c ## ULL)
    
    #define INTMAX_C(c) (c ## LL)
    #define UINTMAX_C(c) (c ## ULL)
    # 5 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/usr/local/share/frama-c/libc/limits.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    /* ISO C: 7.10 and 5.2.4.2.1 */
    
    #define __FC_LIMITS
    
    # 1 "/usr/local/share/frama-c/libc/__fc_machdep.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    # 28 "/usr/local/share/frama-c/libc/limits.h" 2
    
    /* Number of bits in a `char'.	*/
    #define CHAR_BIT __CHAR_BIT
    
    
    /* Minimum and maximum values a `signed char' can hold.  */
    #define SCHAR_MIN __FC_SCHAR_MIN
    #define SCHAR_MAX __FC_SCHAR_MAX
    
    /* Maximum value an `unsigned char' can hold.  (Minimum is 0.)  */
    #define UCHAR_MAX __FC_UCHAR_MAX
    
    /* Minimum and maximum values a `char' can hold.  */
    
    
    
    
    #define CHAR_MIN SCHAR_MIN
    #define CHAR_MAX SCHAR_MAX
    
    
    #define MB_LEN_MAX 16
    
    /* Minimum and maximum values a `signed short int' can hold.  */
    #define SHRT_MIN __FC_SHRT_MIN
    #define SHRT_MAX __FC_SHRT_MAX
    
    /* Maximum value an `unsigned short int' can hold.  (Minimum is 0.)  */
    #define USHRT_MAX __FC_USHRT_MAX
    
    /* Minimum and maximum values a `signed int' can hold.  */
    #define INT_MIN __FC_INT_MIN
    #define INT_MAX __FC_INT_MAX
    
    /* Maximum value an `unsigned int' can hold.  (Minimum is 0.)  */
    #define UINT_MAX __FC_UINT_MAX
    
    /* Minimum and maximum values a `signed long int' can hold.  */
    #define LONG_MAX __FC_LONG_MAX
    #define LONG_MIN __FC_LONG_MIN
    
    /* Maximum value an `unsigned long int' can hold.  (Minimum is 0.)  */
    #define ULONG_MAX __FC_ULONG_MAX
    
    /* Minimum and maximum values a `signed long long int' can hold.  */
    #define LLONG_MAX __FC_LLONG_MAX
    #define LLONG_MIN __FC_LLONG_MIN
    
    /* Maximum value an `unsigned long long int' can hold.  (Minimum is 0.)  */
    #define ULLONG_MAX __FC_ULLONG_MAX
    # 6 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bits.h" 1
    
    #define Bits_defined
    
    # 1 "/usr/local/share/frama-c/libc/stdint.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    /* ISO C: 7.18 */
    # 5 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bits.h" 2
    
    /*@ axiomatic b4fc_btest
     @ {
     @   logic boolean LogicalBitTest(integer v, integer n);
     @   predicate     BitTest (integer v, integer n);
     @ }
     */
    
    #define BytePos(Pos) ((Pos)/8)
    #define LeftBit8(Value,Pos) (BitTest(Value,(7 - (Pos))))
    #define LeftBitInStream(Stream,Pos) (LeftBit8(Stream[BytePos(Pos)],((Pos)%8)))
    #define LeftBit64(Value,Pos) (BitTest(Value,(63 - (Pos))))
    
    /*@
     predicate
     EqualBits{A}(uint8_t* Bitstream, uint64_t Value, integer Start, integer Length) =
     \forall integer i; 0 <= i < Length ==>
     (LeftBitInStream(Bitstream, Start + i) <==> LeftBit64(Value, 64-Length+i));
     */
    
    /*@
     predicate
     NotSet{A}(uint64_t Value, integer Length) =
     \forall integer i; 0 <= i < Length ==>
     !LeftBit64(Value, i);
     */
    
    /*@
     predicate
     IsCopied{A}(uint8_t* Bitstream, uint64_t Value, integer Start, integer Length) =
     \forall integer i; 0 <= i < Length ==>
     (EqualBits(Bitstream, Value, Start, Length) && NotSet(Value, 64-i));
     */
    
    /*@
     predicate
     Unchanged{A}(uint8_t* Bitstream1, uint8_t* Bitstream2, integer Start, integer Length, integer Size) =
     \forall integer i; ((0 <= i < Start ==> (LeftBitInStream(Bitstream1, i) <==> LeftBitInStream(Bitstream2, i))) &&
     (Start+Length <= i < Size ==> (LeftBitInStream(Bitstream1, i) <==> LeftBitInStream(Bitstream2, i))));
     */
    
    /*
     // not used
     lemma BitsAndMore :
     \forall uint64_t x, integer n;
     (0 <= n < 64)  ==>
     ((x < (1 << n)) <==> (\forall integer i; 0 <= i && i < 64-n ==> !LeftBit64(x, i)));
     */
    
    /*
     // not used
     lemma BitsAndEquality :
     \forall uint64_t x, y;
     (\forall integer i; 0 <= i && i < 64 ==> (LeftBit64(x, i) <==> LeftBit64(y, i)))
     ==> (x == y);
     */
    # 7 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Peek.h" 1
    
    
    #define Peek_defined
    
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 1
    # 6 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Peek.h" 2
    
    /*@
     requires \valid_read(Bitstream + (0..BitstreamSize-1));
     requires 0 <= Length <= 64;
     requires Start + Length <= UINT_MAX;
     requires 8 * BitstreamSize <= UINT_MAX;
     
     assigns \nothing;
     
     behavior  invalid_bit_sequence:
     assumes (Start + Length) > 8 * BitstreamSize;
     assigns \nothing;
     ensures \result == 0;
     
     behavior  normal_case:
     assumes (Start + Length) <= 8 * BitstreamSize;
     assigns \nothing;
     
     ensures \forall integer i; 0 <= i < Length ==>
     (LeftBitInStream(Bitstream, Start+i) <==> LeftBit64(\result, 64-Length + i));
     
     ensures EqualBits(Bitstream, \result, Start, Length);
     
     ensures \forall integer i; 0 <= i < 64-Length ==> !LeftBit64(\result, i);
     
     ensures NotSet(\result, 64-Length);
     
     complete behaviors;
     disjoint behaviors;
     */
    uint64_t Bitwalker_Peek(unsigned int Start,
                            unsigned int Length,
                            uint8_t Bitstream[],
                            unsigned int BitstreamSize);
    # 8 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Poke.h" 1
    
    #define Poke_defined
    
    
    
    /*@
     requires writeable_bitstream:
     \valid(Bitstream + (0..BitstreamSize-1));
     requires valid_length: 0 <= Length < 64;
     requires no_overflow_1: Start + Length <= UINT_MAX;
     requires no_overflow_2: 8 * BitstreamSize <= UINT_MAX;
     
     assigns Bitstream[0..BitstreamSize - 1];
     
     behavior  invalid_bit_sequence:
     assumes (Start + Length)  > 8 * BitstreamSize;
     assigns \nothing;
     ensures \result == -1;
     
     behavior  value_too_big:
     assumes (1 << Length) <= Value &&
     (Start + Length) <= 8 * BitstreamSize;
     assigns \nothing;
     ensures \result == -2;
     
     behavior  normal_case:
     assumes Value < (1 << Length) && (Start + Length) <= 8 * BitstreamSize;
     assigns Bitstream[0..BitstreamSize - 1];
     
     ensures \forall integer i; 0 <= i < Length ==>
     (LeftBitInStream(Bitstream, Start+i) <==> LeftBit64(Value,(64-Length)+i));
     
     ensures EqualBits(Bitstream, Value, Start, Length);
     
     ensures \forall integer i; 0 <= i < Start ==>
     (LeftBitInStream(Bitstream, i) <==> \old(LeftBitInStream(Bitstream, i)));
     
     ensures \forall integer i; Start+Length <= i < 8*BitstreamSize ==>
     (LeftBitInStream(Bitstream, i) <==> \old(LeftBitInStream(Bitstream, i)));
     
     ensures Unchanged(Bitstream, \old(Bitstream), Start, Length, 8*BitstreamSize);
     
     ensures \result == 0;
     
     complete behaviors;
     disjoint behaviors;
     */
    int Bitwalker_Poke (unsigned int Start,
                        unsigned int Length,
                        uint8_t Bitstream[],
                        unsigned int BitstreamSize,
                        uint64_t Value);
    # 9 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Init.h" 1
    
    #define INIT_H
    
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Locals.h" 1
    
    #define LOCALS_H
    
    # 1 "/usr/local/share/frama-c/libc/stdint.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    /* ISO C: 7.18 */
    # 5 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Locals.h" 2
    # 1 "/usr/local/share/frama-c/libc/limits.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    /* ISO C: 7.10 and 5.2.4.2.1 */
    # 6 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Locals.h" 2
    
    struct BitwalkerLocals
    {
        uint8_t *Bitstream;
        unsigned int Length;
        unsigned int CurrentBitposition;
    };
    
    typedef struct BitwalkerLocals T_Bitwalker_Incremental_Locals;
    # 5 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Init.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/ValidBitwalker.h" 1
    
    #define ValidBitwalker_define
    
    
    
    /*@
     predicate ValidBitwalker(T_Bitwalker_Incremental_Locals* ptr) =
     \valid(ptr->Bitstream + (0..ptr->Length-1)) &&
     8 * ptr->Length <= UINT_MAX &&
     \separated(ptr->Bitstream + (0..ptr->Length-1), ptr);
     */
    # 6 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Init.h" 2
    
    /*@
     requires \valid(Locals);
     requires \valid(Bitstream + (0..Size-1));
     requires 8 * Size <= UINT_MAX;
     // This must be FirstBitposition <= 8 * Size;
     // requires 8 * FirstBitposition <= Size;
     requires \separated(Bitstream + (0..Size-1), Locals);
     
     assigns  Locals->Bitstream;
     assigns  Locals->Length;
     assigns  Locals->CurrentBitposition;
     
     ensures  Locals->Bitstream == Bitstream;
     ensures  Locals->Length == Size;
     ensures  Locals->CurrentBitposition == FirstBitposition;
     ensures  ValidBitwalker(Locals);
     */
    void Bitwalker_IncrementalWalker_Init(
                                          T_Bitwalker_Incremental_Locals* Locals,
                                          uint8_t Bitstream[],
                                          unsigned int Size,
                                          unsigned int FirstBitposition);
    # 10 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/PeekNext.h" 1
    
    #define PeekNext_included
    
    
    
    
    
    /*@
     requires \valid(Locals);
     requires 0 <= Length <= 64;
     requires ValidBitwalker(Locals);
     requires Locals->CurrentBitposition + Length <= UINT_MAX;
     
     assigns  Locals->CurrentBitposition;
     
     ensures \old(Locals->CurrentBitposition) + Length == Locals->CurrentBitposition;
     
     behavior  invalid_bit_sequence:
     assumes (Locals->CurrentBitposition + Length)  > 8 * Locals->Length;
     assigns  Locals->CurrentBitposition;
     
     ensures \result == 0;
     
     behavior  normal_case:
     assumes (Locals->CurrentBitposition + Length) <= 8 * Locals->Length;
     assigns  Locals->CurrentBitposition;
     
     ensures \forall integer i; 0 <= i < Length ==>
     (LeftBitInStream(\old(Locals->Bitstream), \old(Locals->CurrentBitposition)+i) <==> LeftBit64(\result, 64-Length + i));
     
     ensures EqualBits(\old(Locals->Bitstream), \result, \old(Locals->CurrentBitposition), Length);
     
     ensures \forall integer i; 0 <= i < 64-Length ==> !LeftBit64(\result, i);
     
     ensures NotSet(\result, 64-Length);
     
     complete behaviors;
     disjoint behaviors;
     */
    uint64_t Bitwalker_IncrementalWalker_Peek_Next(
                                                   T_Bitwalker_Incremental_Locals* Locals,
                                                   unsigned int Length);
    # 11 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/PeekFinish.h" 1
    
    #define PEEK_FINISH_H
    
    
    # 1 "/usr/local/share/frama-c/libc/limits.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    /* ISO C: 7.10 and 5.2.4.2.1 */
    # 6 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/PeekFinish.h" 2
    
    /*@
     requires \valid(Locals);
     requires Locals->CurrentBitposition <= INT_MAX;
     
     assigns  \nothing;
     
     ensures  \result == Locals->CurrentBitposition;
     */
    int Bitwalker_IncrementalWalker_Peek_Finish(
                                                T_Bitwalker_Incremental_Locals *Locals);
    # 12 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/PokeNext.h" 1
    
    
    #define PokeNext_included
    
    
    
    
    
    /*@
     requires \valid(Locals);
     requires ValidBitwalker(Locals);
     requires 0 <= Length <= 63;
     requires Locals->CurrentBitposition + Length <= UINT_MAX;
     
     assigns  Locals->Bitstream[0..Locals->Length - 1], Locals->CurrentBitposition;
     
     ensures \old(Locals->CurrentBitposition) + Length == Locals->CurrentBitposition;
     
     behavior  invalid_bit_sequence:
     assumes (Locals->CurrentBitposition + Length) > 8 * Locals->Length;
     ensures \old(Locals->CurrentBitposition) + Length == Locals->CurrentBitposition;
     ensures \result == -1;
     
     behavior  value_too_big:
     assumes (1 << Length) <= Value &&
     (Locals->CurrentBitposition + Length) <= 8 * Locals->Length;
     ensures \old(Locals->CurrentBitposition) + Length == Locals->CurrentBitposition;
     ensures \result == -2;
     
     behavior  normal_case:
     assumes Value < (1 << Length) &&
     (Locals->CurrentBitposition + Length) <= 8 * Locals->Length;
     assigns  Locals->Bitstream[0..Locals->Length - 1], Locals->CurrentBitposition;
     
     ensures \forall integer i; 0 <= i < \old(Locals->CurrentBitposition) ==>
     (LeftBitInStream(Locals->Bitstream, i) <==> \old(LeftBitInStream(Locals->Bitstream, i)));
     
     ensures \forall integer i; Locals->CurrentBitposition < i < 8*Locals->Length  ==>
     (LeftBitInStream(Locals->Bitstream, i) <==> \old(LeftBitInStream(Locals->Bitstream, i)));
     
     ensures Unchanged(Locals->Bitstream, \old(Locals->Bitstream), \old(Locals->CurrentBitposition), Locals->CurrentBitposition, 8*Locals->Length);
     
     ensures \forall integer i; 0 <= i < Length ==>
     (LeftBitInStream(Locals->Bitstream, \old(Locals->CurrentBitposition)+i) <==> LeftBit64(Value, (64-Length)+i));
     
     ensures EqualBits(Locals->Bitstream, Value, \old(Locals->CurrentBitposition), Length);
     
     ensures \result == 0;
     
     complete behaviors;
     disjoint behaviors;
     */
    int Bitwalker_IncrementalWalker_Poke_Next(
                                              T_Bitwalker_Incremental_Locals* Locals,
                                              unsigned int Length,
                                              uint64_t Value);
    # 13 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/PokeFinish.h" 1
    
    
    #define POKE_FINISH_H
    
    
    
    /*@
     requires  \valid(Locals);
     requires  Locals->CurrentBitposition <= INT_MAX;
     
     assigns   \nothing;
     
     ensures \result == Locals->CurrentBitposition;
     */
    int Bitwalker_IncrementalWalker_Poke_Finish(
                                                T_Bitwalker_Incremental_Locals *Locals);
    # 14 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Bitwalker.h" 2
    # 24 "Adhesion_Factor.h" 2
    # 1 "/usr/local/share/frama-c/libc/stdint.h" 1
    /**************************************************************************/
    /*                                                                        */
    /*  This file is part of Frama-C.                                         */
    /*                                                                        */
    /*  Copyright (C) 2007-2014                                               */
    /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
    /*         alternatives)                                                  */
    /*                                                                        */
    /*  you can redistribute it and/or modify it under the terms of the GNU   */
    /*  Lesser General Public License as published by the Free Software       */
    /*  Foundation, version 2.1.                                              */
    /*                                                                        */
    /*  It is distributed in the hope that it will be useful,                 */
    /*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
    /*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
    /*  GNU Lesser General Public License for more details.                   */
    /*                                                                        */
    /*  See the GNU Lesser General Public License version 2.1                 */
    /*  for more details (enclosed in the file licenses/LGPLv2.1).            */
    /*                                                                        */
    /**************************************************************************/
    
    /* ISO C: 7.18 */
    # 25 "Adhesion_Factor.h" 2
    # 1 "../opnETCS_Variables.h" 1
    
    #define NESTINGMARK_oETCS_Variables
    
    
    /* =============================================================================
     Formalization of Subset-026-7 (Chapter 7: ERTMS/ETCS language)
     
     - Name: opnETCS_Variables.h
     - Description: UNISIG SUBSET-026-7, ISSUE : 3.3.0, 3.5 ERTMS/ETCS language)
     - Copyright (c) Siemens AG, 2014, All Rights Reserved
     
     - Licensed under the EUPL V.1.1 ( http://joinup.ec.europa.eu/software/page/eupl/licence-eupl )
     - Gist URL: none
     - Cryptography: No
     - Author(s): SiemensRailAutomation
     
     Disclaimer:
     
     The use of this software is limited to NON-vital applications.
     It has NOT been developed for vital operation purposes and MUST NOT be used for applications
     which may cause harm to people, physical accidents or financial loss.
     
     THEREFORE, NO LIABILITY WILL BE GIVEN FOR SUCH AND ANY OTHER KIND OF USE.
     ============================================================================= */
    
    float A_NVMAXREDADH1 /* MinVal = 0.0, MaxVal = 3.15 */ ;
    float A_NVMAXREDADH2 /* MinVal = 0.0, MaxVal = 3.15 */ ;
    float A_NVMAXREDADH3 /* MinVal = 0.0, MaxVal = 3.15 */ ;
    float A_NVP12 /* MinVal = 0.0, MaxVal = 3.15 */ ;
    float A_NVP23 /* MinVal = 0.0, MaxVal = 3.15 */ ;
    int D_ADHESION /* MinVal = 0, MaxVal = 32767 */ ;
    int D_AXLELOAD /* MinVal = 0, MaxVal = 32767 */ ;
    int D_CURRENT /* MinVal = 0, MaxVal = 32767 */ ;
    int D_CYCLOC /* MinVal = 0, MaxVal = 32766 */ // 1111 1111 = The_train_has_not_to_report_cyclically_its_position
    ;
    int D_DP /* MinVal = 0, MaxVal = 32767 */ ;
    int D_EMERGENCYSTOP /* MinVal = 0, MaxVal = 32767 */ ;
    int D_ENDTIMERSTARTLOC /* MinVal = 0, MaxVal = 32767 */ ;
    int D_GRADIENT /* MinVal = 0, MaxVal = 32767 */ ;
    int D_INFILL /* MinVal = 0, MaxVal = 32767 */ ;
    int D_LEVELTR /* MinVal = 0, MaxVal = 32766 */ // 32767 = Now_(The_level_transition_is_performed_upon_receipt_of_the_order)
    ;
    int D_LINK /* MinVal = 0, MaxVal = 32767 */ ;
    int D_LOC /* MinVal = 0, MaxVal = 32767 */ ;
    int D_LOOP /* MinVal = 0, MaxVal = 32766 */ // 32767 = Distance_not_known
    ;
    int D_LRBG /* MinVal = 0, MaxVal = 32766 */ // 32767 = Unknown
    ;
    int D_LX /* MinVal = 0, MaxVal = 32767 */ ;
    int D_MAMODE /* MinVal = 0, MaxVal = 32767 */ ;
    int D_NVOVTRP /* MinVal = 0, MaxVal = 32767 */ ;
    int D_NVPOTRP /* MinVal = 0, MaxVal = 32767 */ ;
    int D_NVROLL /* MinVal = 0, MaxVal = 32766 */ // 32767 = infinite
    ;
    int D_NVSTFF /* MinVal = 0, MaxVal = 32766 */ // 32767 = infinite
    ;
    int D_OL /* MinVal = 0, MaxVal = 32767 */ ;
    int D_PBD /* MinVal = 0, MaxVal = 32767 */ ;
    int D_PBDSR /* MinVal = 0, MaxVal = 32767 */ ;
    int D_POSOFF /* MinVal = 0, MaxVal = 32767 */ ;
    int D_RBCTR /* MinVal = 0, MaxVal = 32767 */ ;
    int D_REF /* MinVal = -32768, MaxVal = 32767 */ ;
    int D_REVERSE /* MinVal = 0, MaxVal = 32766 */ // 32767 = represents_infinite
    ;
    int D_SECTIONTIMERSTOPLOC /* MinVal = 0, MaxVal = 32767 */ ;
    int D_SR /* MinVal = 0, MaxVal = 32766 */ // 32767 = Represents_infinite
    ;
    int D_STARTOL /* MinVal = 0, MaxVal = 32767 */ ;
    int D_STARTREVERSE /* MinVal = 0, MaxVal = 32767 */ ;
    int D_STATIC /* MinVal = 0, MaxVal = 32767 */ ;
    int D_SUITABILITY /* MinVal = 0, MaxVal = 32767 */ ;
    int D_TAFDISPLAY /* MinVal = 0, MaxVal = 32767 */ ;
    int D_TEXTDISPLAY /* MinVal = 0, MaxVal = 32766 */ // 32767 = The_display_of_the_text_shall_not_be_distance_limited
    ;
    int D_TRACKINIT /* MinVal = 0, MaxVal = 32767 */ ;
    int D_TRACKCOND /* MinVal = 0, MaxVal = 32767 */ ;
    int D_TRACTION /* MinVal = 0, MaxVal = 32767 */ ;
    int D_TSR /* MinVal = 0, MaxVal = 32767 */ ;
    int D_VALIDNV /* MinVal = 0, MaxVal = 32766 */ // 32767 = Now_(National_Values_are_immediately_applicable)
    ;
    int G_A /* MinVal = 0, MaxVal = 254 */ // 255 = Non_numerical_value_telling_that_the_current_gradient_description_ends_at_D_GRADIENT(n)
    ;
    int G_PBDSR /* MinVal = 0, MaxVal = 255 */ ;
    int G_TSR /* MinVal = 0, MaxVal = 255 */ ;
    int L_ACKLEVELTR /* MinVal = 0, MaxVal = 32767 */ ;
    int L_ACKMAMODE /* MinVal = 0, MaxVal = 32767 */ ;
    int L_ADHESION /* MinVal = 0, MaxVal = 32767 */ ;
    int L_AXLELOAD /* MinVal = 0, MaxVal = 32767 */ ;
    int L_DOUBTOVER /* MinVal = 0, MaxVal = 32766 */ // 32767 = Unknown
    ;
    int L_DOUBTUNDER /* MinVal = 0, MaxVal = 32766 */ // 32767 = Unknown
    ;
    int L_ENDSECTION /* MinVal = 0, MaxVal = 32767 */ ;
    int L_LOOP /* MinVal = 0, MaxVal = 32766 */ // 32767 = Length_not_known
    ;
    int L_LX /* MinVal = 0, MaxVal = 32767 */ ;
    int L_MAMODE /* MinVal = 0, MaxVal = 32766 */ // 32767 = Infinite_length
    ;
    int L_MESSAGE /* MinVal = 0, MaxVal = 1023 */ ;
    typedef enum {
        L_NVKRINT_0m = 0 ,
        L_NVKRINT_25m = 1 ,
        L_NVKRINT_50m = 2 ,
        L_NVKRINT_75m = 3 ,
        L_NVKRINT_100m = 4 ,
        L_NVKRINT_150m = 5 ,
        L_NVKRINT_200m = 6 ,
        L_NVKRINT_300m = 7 ,
        L_NVKRINT_400m = 8 ,
        L_NVKRINT_500m = 9 ,
        L_NVKRINT_600m = 10 ,
        L_NVKRINT_700m = 11 ,
        L_NVKRINT_800m = 12 ,
        L_NVKRINT_900m = 13 ,
        L_NVKRINT_1000m = 14 ,
        L_NVKRINT_1100m = 15 ,
        L_NVKRINT_1200m = 16 ,
        L_NVKRINT_1300m = 17 ,
        L_NVKRINT_1400m = 18 ,
        L_NVKRINT_1500m = 19 ,
        L_NVKRINT_1600m = 20 ,
        L_NVKRINT_1700m = 21 ,
        L_NVKRINT_1800m = 22 ,
        L_NVKRINT_1900m = 23 ,
        L_NVKRINT_2000m = 24 ,
        L_NVKRINT_2100m = 25 ,
        L_NVKRINT_2200m = 26 ,
        L_NVKRINT_2300m = 27 ,
        L_NVKRINT_2400m = 28 ,
        L_NVKRINT_2500m = 29 ,
        L_NVKRINT_2600m = 30 ,
        L_NVKRINT_2700m = 31
    } T_l_nvkrint ;
    int L_PACKET /* MinVal = 0, MaxVal = 8191 */ ;
    int L_PBDSR /* MinVal = 0, MaxVal = 32767 */ ;
    int L_REVERSEAREA /* MinVal = 0, MaxVal = 32767 */ ;
    int L_SECTION /* MinVal = 0, MaxVal = 32767 */ ;
    int L_STOPLX /* MinVal = 0, MaxVal = 32767 */ ;
    int L_TAFDISPLAY /* MinVal = 0, MaxVal = 32767 */ ;
    int L_TEXT /* MinVal = 0, MaxVal = 255 */ ;
    int L_TEXTDISPLAY /* MinVal = 0, MaxVal = 32766 */ // 32767 = The_display_of_the_text_shall_not_be_distance_limited
    ;
    int L_TRACKCOND /* MinVal = 0, MaxVal = 32767 */ ;
    int L_TRAIN /* MinVal = 0, MaxVal = 4095 */ ;
    int L_TRAININT /* MinVal = 0, MaxVal = 32767 */ ;
    int L_TSR /* MinVal = 0, MaxVal = 32767 */ ;
    typedef enum {
        M_ACK_No_acknowledgement_required = 0 ,
        M_ACK_Acknowledgement_required = 1
    } T_m_ack ;
    typedef enum {
        M_ADHESION_Slippery_rail = 0 ,
        M_ADHESION_Non_slippery_rail = 1
    } T_m_adhesion ;
    typedef enum {
        M_AIRTIGHT_Not_fitted = 0 ,
        M_AIRTIGHT_Fitted = 1
    } T_m_airtight ;
    typedef enum {
        M_AXLELOADCAT_A = 0 ,
        M_AXLELOADCAT_HS17 = 1 ,
        M_AXLELOADCAT_B1 = 2 ,
        M_AXLELOADCAT_B2 = 3 ,
        M_AXLELOADCAT_C2 = 4 ,
        M_AXLELOADCAT_C3 = 5 ,
        M_AXLELOADCAT_C4 = 6 ,
        M_AXLELOADCAT_D2 = 7 ,
        M_AXLELOADCAT_D3 = 8 ,
        M_AXLELOADCAT_D4 = 9 ,
        M_AXLELOADCAT_D4XL = 10 ,
        M_AXLELOADCAT_E4 = 11 ,
        M_AXLELOADCAT_E5 = 12
    } T_m_axleloadcat ;
    int M_CURRENT /* MinVal = 0, MaxVal = 10000 */ // 1023 = No_restriction_for_current_consumption
    ;
    typedef enum {
        M_DUP_No_duplicates = 0 ,
        M_DUP_This_balise_is_a_duplicate_of_the_next_balise = 1 ,
        M_DUP_This_balise_is_a_duplicate_of_the_previous_balise = 2
    } T_m_dup ;
    typedef enum {
        M_ERROR_Balise_group_linking_consistency_error = 0 ,
        M_ERROR_Linked_balise_group_message_consistency_erro = 1 ,
        M_ERROR_Unlinked_balise_group_message_consistency_error = 2 ,
        M_ERROR_Radio_message_consistency_error = 3 ,
        M_ERROR_Radio_sequence_error = 4 ,
        M_ERROR_Radio_safe_radio_connection_error = 5 ,
        M_ERROR_Safety_critical_failure = 6 ,
        M_ERROR_Double_linking_error = 7 ,
        M_ERROR_Double_repositioning_error = 8
    } T_m_error ;
    typedef enum {
        M_LEVEL_Level_0 = 0 ,
        M_LEVEL_Level_NTC_specified_by_NID_NTC = 1 ,
        M_LEVEL_Level_1 = 2 ,
        M_LEVEL_Level_2 = 3 ,
        M_LEVEL_Level_3 = 4
    } T_m_level ;
    typedef enum {
        M_LEVELTEXTDISPLAY_Level_0 = 0 ,
        M_LEVELTEXTDISPLAY_Level_NTC_specified_by_NID_NTC = 1 ,
        M_LEVELTEXTDISPLAY_Level_1 = 2 ,
        M_LEVELTEXTDISPLAY_Level_2 = 3 ,
        M_LEVELTEXTDISPLAY_Level_3 = 4 ,
        M_LEVELTEXTDISPLAY_The_display_of_the_text_shall_not_be_limited_by_the_level = 5
    } T_m_leveltextdisplay ;
    typedef enum {
        M_LEVELTR_Level_0 = 0 ,
        M_LEVELTR_Level_NTC_specified_by_NID_NTC = 1 ,
        M_LEVELTR_Level_1 = 2 ,
        M_LEVELTR_Level_2 = 3 ,
        M_LEVELTR_Level_3 = 4
    } T_m_leveltr ;
    typedef enum {
        M_LINEGAUGE_G1 = 1 ,
        M_LINEGAUGE_GA = 2 ,
        M_LINEGAUGE_GB = 4 ,
        M_LINEGAUGE_GC = 8
    } T_m_linegauge ;
    typedef enum {
        M_LOADINGGAUGE_The_train_does_not_fit_to_any_of_the_interoperable_loading_gauge_profiles = 0 ,
        M_LOADINGGAUGE_G1 = 1 ,
        M_LOADINGGAUGE_GA = 2 ,
        M_LOADINGGAUGE_GB = 3 ,
        M_LOADINGGAUGE_GC = 4
    } T_m_loadinggauge ;
    typedef enum {
        M_LOC_Now = 0 ,
        M_LOC_Every_LRBG_compliant_balise_group = 1 ,
        M_LOC_Do_not_send_position_report_on_passage_of_LRBG_compliant_balise_group = 2
    } T_m_loc ;
    typedef enum {
        M_MAMODE_On_Sight = 0 ,
        M_MAMODE_Shunting = 1 ,
        M_MAMODE_Limited_Supervision = 2
    } T_m_mamode ;
    int M_MCOUNT /* MinVal = 0, MaxVal = 253 */ // 254 = The_telegram_never_fits_any_message_of_the_group
    // 255 = The_telegram_fits_with_all_telegrams_of_the_same_balise_group
    ;
    typedef enum {
        M_MODE_Full_Supervision = 0 ,
        M_MODE_On_Sight = 1 ,
        M_MODE_Staff_Responsible = 2 ,
        M_MODE_Shunting = 3 ,
        M_MODE_Unfitted = 4 ,
        M_MODE_Sleeping = 5 ,
        M_MODE_Stand_By = 6 ,
        M_MODE_Trip = 7 ,
        M_MODE_Post_Trip = 8 ,
        M_MODE_System_Failure = 9 ,
        M_MODE_Isolation = 10 ,
        M_MODE_Non_Leading = 11 ,
        M_MODE_Limited_Supervision = 12 ,
        M_MODE_National_System = 13 ,
        M_MODE_Reversing = 14 ,
        M_MODE_Passive_Shunting = 15
    } T_m_mode ;
    typedef enum {
        M_MODETEXTDISPLAY_Full_Supervision = 0 ,
        M_MODETEXTDISPLAY_On_Sight = 1 ,
        M_MODETEXTDISPLAY_Staff_Responsible = 2 ,
        M_MODETEXTDISPLAY_Unfitted = 4 ,
        M_MODETEXTDISPLAY_Stand_By = 6 ,
        M_MODETEXTDISPLAY_Trip = 7 ,
        M_MODETEXTDISPLAY_Post_Trip = 8 ,
        M_MODETEXTDISPLAY_Non_Leading = 11 ,
        M_MODETEXTDISPLAY_Limited_Supervision = 12 ,
        M_MODETEXTDISPLAY_Reversing = 14 ,
        M_MODETEXTDISPLAY_The_display_of_the_text_shall_not_be_limited_by_the_mode = 15
    } T_m_modetextdisplay ;
    float M_NVAVADH /* MinVal = 0.0, MaxVal = 1.0 */ ;
    typedef enum {
        M_NVCONTACT_Train_trip = 0 ,
        M_NVCONTACT_Apply_service_brake = 1 ,
        M_NVCONTACT_No_Reaction = 2
    } T_m_nvcontact ;
    typedef enum {
        M_NVDERUN_No = 0 ,
        M_NVDERUN_Yes = 1
    } T_m_nvderun ;
    typedef enum {
        M_NVEBCL_Confidence_level_50 = 0 ,
        M_NVEBCL_Confidence_level_90 = 1 ,
        M_NVEBCL_Confidence_level_99 = 2 ,
        M_NVEBCL_Confidence_level_99_9 = 3 ,
        M_NVEBCL_Confidence_level_99_99 = 4 ,
        M_NVEBCL_Confidence_level_99_999 = 5 ,
        M_NVEBCL_Confidence_level_99_9999 = 6 ,
        M_NVEBCL_Confidence_level_99_99999 = 7 ,
        M_NVEBCL_Confidence_level_99_999999 = 8 ,
        M_NVEBCL_Confidence_level_99_9999999 = 9
    } T_m_nvebcl ;
    float M_NVKRINT /* MinVal = 0.0, MaxVal = 1.5 */ ;
    float M_NVKTINT /* MinVal = 0.0, MaxVal = 1.5 */ ;
    float M_NVKVINT /* MinVal = 0.0, MaxVal = 2.5 */ ;
    typedef enum {
        M_PLATFORM_200_mm = 0 ,
        M_PLATFORM_300380_mm = 1 ,
        M_PLATFORM_550_mm = 2 ,
        M_PLATFORM_580_mm = 3 ,
        M_PLATFORM_680_mm = 4 ,
        M_PLATFORM_685_mm = 5 ,
        M_PLATFORM_730_mm = 6 ,
        M_PLATFORM_760_mm = 7 ,
        M_PLATFORM_840_mm = 8 ,
        M_PLATFORM_900_mm = 9 ,
        M_PLATFORM_915_mm = 10 ,
        M_PLATFORM_920_mm = 11 ,
        M_PLATFORM_960_mm = 12 ,
        M_PLATFORM_1100_mm = 13
    } T_m_platform ;
    int M_POSITION /* MinVal = 0, MaxVal = 9999999 */ // 16777215 = No_more_geographical_position_calculation_after_this_reference_location
    ;
    typedef enum {
        M_TRACKCOND_Non_stopping_area_Initial_state_is_stopping_permitted = 0 ,
        M_TRACKCOND_Tunnel_stopping_area_Initial_state_is_no_tunnel_stopping_area = 1 ,
        M_TRACKCOND_Sound_horn_Initial_state_is_is_no_request_for_sound_horn = 2 ,
        M_TRACKCOND_Powerless_section_Lower_pantograph_Initial_state_is_not_powerless_section = 3 ,
        M_TRACKCOND_Radio_hole_stop_supervising_T_NVCONTACT_Initial_state_is_supervise_T_NVCONTACT = 4 ,
        M_TRACKCOND_Air_tightness_Initial_state_is_no_request_for_air_tightness = 5 ,
        M_TRACKCOND_Switch_off_regenerative_brake_Initial_state_is_regenerative_brake_on = 6 ,
        M_TRACKCOND_Switch_off_eddy_current_brake_for_service_brake_Initial_state_is_eddy_current_brake_for_service_brake_on = 7 ,
        M_TRACKCOND_Switch_off_magnetic_shoe_brake_Initial_state_is_magnetic_shoe_brake_on = 8 ,
        M_TRACKCOND_Powerless_section_switch_off_the_main_power_switch_Initial_state_is_not_powerless_section = 9 ,
        M_TRACKCOND_Switch_off_eddy_current_brake_for_emergency_brake_Initial_state_is_eddy_current_brake_for_emergency_brake_on = 10
    } T_m_trackcond ;
    typedef enum {
        M_VOLTAGE_Line_not_fitted_with_any_traction_system = 0 ,
        M_VOLTAGE_AC_25_kV_50_Hz = 1 ,
        M_VOLTAGE_AC_15_kV_16_7_Hz = 2 ,
        M_VOLTAGE_DC_3_kV = 3 ,
        M_VOLTAGE_DC_1_5_kV = 4 ,
        M_VOLTAGE_DC_600_or_750_V = 5
    } T_m_voltage ;
    typedef enum {
        M_VERSION_Previous_versions_according_to_e_g_EEIG_SRS_and_UIC_A200_SRS = 0 ,
        M_VERSION_Version_1_0_introduced_in_SRS_1_2_0_and_reused_in_SRSs_2_0_0_and_2_2_2_and_2_3_0 = 16 ,
        M_VERSION_Version_1_1_introduced_in_SRS_3_3_0 = 17 ,
        M_VERSION_Version_2_0_introduced_in_SRS_3_3_0 = 32
    } T_m_version ;
    int N_AXLE /* MinVal = 0, MaxVal = 1022 */ // 1023 = Unknown
    ;
    int N_ITER /* MinVal = 0, MaxVal = 31 */ ;
    typedef enum {
        N_PIG_I_am_the_1st = 0 ,
        N_PIG_I_am_the_2nd = 1 ,
        N_PIG_I_am_the_3rd = 2 ,
        N_PIG_I_am_the_4th = 3 ,
        N_PIG_I_am_the_5th = 4 ,
        N_PIG_I_am_the_6th = 5 ,
        N_PIG_I_am_the_7th = 6 ,
        N_PIG_I_am_the_8th = 7
    } T_n_pig ;
    typedef enum {
        N_TOTAL_1_balise_in_the_group = 0 ,
        N_TOTAL_2_balises_in_the_group = 1 ,
        N_TOTAL_3_balises_in_the_group = 2 ,
        N_TOTAL_4_balises_in_the_group = 3 ,
        N_TOTAL_5_balises_in_the_group = 4 ,
        N_TOTAL_6_balises_in_the_group = 5 ,
        N_TOTAL_7_balises_in_the_group = 6 ,
        N_TOTAL_8_balises_in_the_group = 7
    } T_n_total ;
    typedef enum {
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_80_mm = 0 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_100_mm = 1 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_130_mm = 2 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_150_mm = 3 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_165_mm = 4 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_180_mm = 5 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_210_mm = 6 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_225_mm = 7 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_245_mm = 8 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_275_mm = 9 ,
        NC_CDDIFF_Specific_SSP_applicable_to_Cant_Deficiency_300_mm = 10
    } T_nc_cddiff ;
    typedef enum {
        NC_CDTRAIN_Cant_Deficiency_80_mm = 0 ,
        NC_CDTRAIN_Cant_Deficiency_100_mm = 1 ,
        NC_CDTRAIN_Cant_Deficiency_130_mm = 2 ,
        NC_CDTRAIN_Cant_Deficiency_150_mm = 3 ,
        NC_CDTRAIN_Cant_Deficiency_165_mm = 4 ,
        NC_CDTRAIN_Cant_Deficiency_180_mm = 5 ,
        NC_CDTRAIN_Cant_Deficiency_210_mm = 6 ,
        NC_CDTRAIN_Cant_Deficiency_225_mm = 7 ,
        NC_CDTRAIN_Cant_Deficiency_245_mm = 8 ,
        NC_CDTRAIN_Cant_Deficiency_275_mm = 9 ,
        NC_CDTRAIN_Cant_Deficiency_300_mm = 10
    } T_nc_cdtrain ;
    int NC_DIFF /* MinVal = 0, MaxVal = 15 */ // 0 = Specific_SSP_applicable_to_Freight_train_braked_in_P_position
    // 1 = Specific_SSP_applicable_to_Freight_train_braked_in_G_position
    // 2 = Specific_SSP_applicable_to_Passenger_train
    ;
    typedef enum {
        NC_TRAIN_Train_does_not_belong_to_any_of_the_Other_International_Train_Category = 0 ,
        NC_TRAIN_Freight_train_braked_in_P_position = 1 ,
        NC_TRAIN_Freight_train_braked_in_G_position = 2 ,
        NC_TRAIN_Passenger_train = 4
    } T_nc_train ;
    int NID_BG /* MinVal = 0, MaxVal = 16382 */ // 16383 = Identity_is_unknown_(only_to_be_used_for_Linking_information)
    ;
    int NID_C /* MinVal = 0, MaxVal = 1023 */ ;
    int NID_CTRACTION /* MinVal = 0, MaxVal = 1023 */ ;
    int NID_EM ;
    int NID_ENGINE ;
    int NID_LOOP /* MinVal = 0, MaxVal = 16383 */ ;
    int NID_LRBG // 16777215 = Unknown
    ;
    int NID_LTRBG ;
    int NID_LX /* MinVal = 0, MaxVal = 255 */ // 0-126 = Reserved_for_non_RBC_transmission_(balise_loop_or_radio_infill)
    // 127-255 = Reserved_for_RBC_transmission
    ;
    int NID_MESSAGE /* MinVal = 0, MaxVal = 255 */ ;
    int NID_MN /* MinVal = 0, MaxVal = 999999 */ // A-E = Not_Used
    // F = Use_value_F_for_digit_to_indicate_no_digit_(if_number_shorter_than_6_digits)
    ;
    int NID_OPERATIONAL /* MinVal = 0, MaxVal = 99999999 */ // F = Use_value_F_for_digit_to_indicate_no_digit_(if_number_shorter_than_8_digits)
    ;
    int NID_PACKET /* MinVal = 0, MaxVal = 255 */ ;
    int NID_PRVLRBG // 16777215 = unknown
    ;
    int NID_RADIO /* MinVal = 0, MaxVal = 9999999999999999 */ // A-E = Not_Used
    // F = Use_value_F_for_digit_to_indicate_no_digit_(if_number_shorter_than_16_digits)
    // FFFF FFFF FFFF FFFF = Use_the_short_number_stored_onboard
    ;
    int NID_RBC /* MinVal = 0, MaxVal = 16382 */ // 16383 = Contact_last_known_RBC
    ;
    int NID_RIU /* MinVal = 0, MaxVal = 16383 */ ;
    int NID_NTC ;
    int NID_TEXTMESSAGE /* MinVal = 0, MaxVal = 255 */ ;
    int NID_TSR /* MinVal = 0, MaxVal = 255 */ // 0-126 = Reserved_for_non_RBC_transmission_(balise_loop_or_radio_infill)
    // 127-254 = Reserved_for_RBC_transmission
    // 255 = Nonrevocable_speed_restriction_(applicable_for_all_transmission_media)
    ;
    int NID_VBCMK /* MinVal = 0, MaxVal = 63 */ ;
    int NID_XUSER /* MinVal = 0, MaxVal = 511 */ ;
    typedef enum {
        Q_ASPECT_Stop_if_in_SH_mode = 0 ,
        Q_ASPECT_Go_if_in_SH_mode = 1
    } T_q_aspect ;
    typedef enum {
        Q_CONFTEXTDISPLAY_Driver_acknowledgement_always_ends_the_text_display_regardless_of_the_end_condition = 0 ,
        Q_CONFTEXTDISPLAY_Driver_acknowledgement_is_an_additional_condition_to_end_the_display = 1
    } T_q_conftextdisplay ;
    typedef enum {
        Q_DANGERPOINT_No_danger_point_information = 0 ,
        Q_DANGERPOINT_Danger_point_information_to_follow = 1
    } T_q_dangerpoint ;
    typedef enum {
        Q_DIFF_Cant_Deficiency_specific_category = 0 ,
        Q_DIFF_Other_specific_category_replaces_the_Cant_Deficiency_SSP = 1 ,
        Q_DIFF_Other_specific_category_does_not_replace_the_Cant_Deficiency_SSP = 2
    } T_q_diff ;
    typedef enum {
        Q_DIR_Reverse = 0 ,
        Q_DIR_Nominal = 1 ,
        Q_DIR_Both_directions = 2
    } T_q_dir ;
    typedef enum {
        Q_DIRLRBG_Reverse = 0 ,
        Q_DIRLRBG_Nominal = 1 ,
        Q_DIRLRBG_Unknown = 2
    } T_q_dirlrbg ;
    typedef enum {
        Q_DIRTRAIN_Reverse = 0 ,
        Q_DIRTRAIN_Nominal = 1 ,
        Q_DIRTRAIN_Unknown = 2
    } T_q_dirtrain ;
    typedef enum {
        Q_DLRBG_Reverse = 0 ,
        Q_DLRBG_Nominal = 1 ,
        Q_DLRBG_Unknown = 2
    } T_q_dlrbg ;
    typedef enum {
        Q_EMERGENCYSTOP_Conditional_Emergency_Stop_accepted_with_update_of_EOA = 0 ,
        Q_EMERGENCYSTOP_Conditional_Emergency_Stop_accepted_with_no_update_of_EOA = 1 ,
        Q_EMERGENCYSTOP_Unconditional_Emergency_Stop_accepted = 2 ,
        Q_EMERGENCYSTOP_Emergency_stop = 3
    } T_q_emergencystop ;
    typedef enum {
        Q_ENDTIMER_No_End_section_timer_information = 0 ,
        Q_ENDTIMER_End_section_timer_information_to_follow = 1
    } T_q_endtimer ;
    typedef enum {
        Q_FRONT_Train_length_delay_on_validity_end_point_of_profile_element = 0 ,
        Q_FRONT_No_train_length_delay_on_validity_end_point_of_profile_element = 1
    } T_q_front ;
    typedef enum {
        Q_GDIR_downhill = 0 ,
        Q_GDIR_uphill = 1
    } T_q_gdir ;
    typedef enum {
        Q_INFILL_Enter = 0 ,
        Q_INFILL_Exit = 1
    } T_q_infill ;
    typedef enum {
        Q_LENGTH_No_train_integrity_information_available = 0 ,
        Q_LENGTH_Train_integrity_confirmed_by_integrity_monitoring_device = 1 ,
        Q_LENGTH_Train_integrity_confirmed_by_driver = 2 ,
        Q_LENGTH_Train_integrity_lost = 3
    } T_q_length ;
    typedef enum {
        Q_LGTLOC_Min_safe_rear_end = 0 ,
        Q_LGTLOC_Max_safe_front_end = 1
    } T_q_lgtloc ;
    typedef enum {
        Q_LINK_Unlinked = 0 ,
        Q_LINK_Linked = 1
    } T_q_link ;
    int Q_LOCACC /* MinVal = 0, MaxVal = 63 */ ;
    typedef enum {
        Q_LINKORIENTATION_The_balise_group_is_seen_by_the_train_in_reverse_direction = 0 ,
        Q_LINKORIENTATION_The_balise_group_is_seen_by_the_train_in_nominal_direction = 1
    } T_q_linkorientation ;
    typedef enum {
        Q_LINKREACTION_Train_trip = 0 ,
        Q_LINKREACTION_Apply_service_brake = 1 ,
        Q_LINKREACTION_No_Reaction = 2
    } T_q_linkreaction ;
    typedef enum {
        Q_LOOPDIR_Opposite = 0 ,
        Q_LOOPDIR_Same = 1
    } T_q_loopdir ;
    typedef enum {
        Q_LXSTATUS_LX_is_protected = 0 ,
        Q_LXSTATUS_LX_is_not_protected = 1
    } T_q_lxstatus ;
    typedef enum {
        Q_MAMODE_as_the_EOA = 0 ,
        Q_MAMODE_as_both_the_EOA_and_SvL = 1
    } T_q_mamode ;
    typedef enum {
        Q_MARQSTREASON_Start_selected_by_driver = 1 ,
        Q_MARQSTREASON_Time_before_reaching_preindication_location_for_the_EOA_or_LOA_reached = 2 ,
        Q_MARQSTREASON_Time_before_a_section_timer_or_LOA_speed_timer_expires_reached = 4 ,
        Q_MARQSTREASON_Track_description_deleted = 8 ,
        Q_MARQSTREASON_TAF_up_to_level_2_or_3_transition_location = 16
    } T_q_marqstreason ;
    typedef enum {
        Q_MEDIA_Balise = 0 ,
        Q_MEDIA_Loop = 1
    } T_q_media ;
    typedef enum {
        Q_MPOSITION_Opposite = 0 ,
        Q_MPOSITION_Same = 1
    } T_q_mposition ;
    typedef enum {
        Q_NEWCOUNTRY_Same_country__or__railway_administration_no_NID_C_follows = 0 ,
        Q_NEWCOUNTRY_Not_the_same_country__or__railway_administration_NID_C_follows = 1
    } T_q_newcountry ;
    typedef enum {
        Q_NVDRIVER_ADHES_Not_allowed = 0 ,
        Q_NVDRIVER_ADHES_Allowed = 1
    } T_q_nvdriver_adhes ;
    typedef enum {
        Q_NVEMRRLS_Revoke_emergency_brake_command_at_standstill = 0 ,
        Q_NVEMRRLS_Revoke_emergency_brake_command_when_permitted_speed_supervision_limit_is_no_longer_exceeded = 1
    } T_q_nvemrrls ;
    typedef enum {
        Q_NVGUIPERM_No = 0 ,
        Q_NVGUIPERM_Yes = 1
    } T_q_nvguiperm ;
    typedef enum {
        Q_NVINHSMICPERM_No = 0 ,
        Q_NVINHSMICPERM_Yes = 1
    } T_q_nvinhsmicperm ;
    typedef enum {
        Q_NVKINT_No_integrated_correction_factors_follow = 0 ,
        Q_NVKINT_Integrated_correction_factors_follow = 1
    } T_q_nvkint ;
    typedef enum {
        Q_NVKVINTSET_Freight_trains = 0 ,
        Q_NVKVINTSET_Conventional_passenger_trains = 1
    } T_q_nvkvintset ;
    int Q_NVLOCACC /* MinVal = 0, MaxVal = 63 */ ;
    typedef enum {
        Q_NVSBFBPERM_No = 0 ,
        Q_NVSBFBPERM_Yes = 1
    } T_q_nvsbfbperm ;
    typedef enum {
        Q_NVSBTSMPERM_No = 0 ,
        Q_NVSBTSMPERM_Yes = 1
    } T_q_nvsbtsmperm ;
    typedef enum {
        Q_ORIENTATION_The_balise_group_has_been_passed_by_the_train_in_reverse_direction = 0 ,
        Q_ORIENTATION_The_balise_group_has_been_passed_by_the_train_in_nominal_direction = 1
    } T_q_orientation ;
    typedef enum {
        Q_OVERLAP_No_overlap_information = 0 ,
        Q_OVERLAP_Overlap_information_to_follow = 1
    } T_q_overlap ;
    typedef enum {
        Q_PBDSR_EB_intervention_requested = 0 ,
        Q_PBDSR_SB_intervention_requested = 1
    } T_q_pbdsr ;
    typedef enum {
        Q_PLATFORM_Platform_on_left_side = 0 ,
        Q_PLATFORM_Platform_on_right_side = 1 ,
        Q_PLATFORM_Platform_on_both_sides = 2
    } T_q_platform ;
    typedef enum {
        Q_RBC_Terminate_communication_session = 0 ,
        Q_RBC_Establish_communication_session = 1
    } T_q_rbc ;
    typedef enum {
        Q_RIU_Terminate_communication_session = 0 ,
        Q_RIU_Establish_communication_session = 1
    } T_q_riu ;
    typedef enum {
        Q_SCALE_10_cm_scale = 0 ,
        Q_SCALE_1_m_scale = 1 ,
        Q_SCALE_10_m_scale = 2
    } T_q_scale ;
    typedef enum {
        Q_SECTIONTIMER_No_Section_Timer_information = 0 ,
        Q_SECTIONTIMER_Section_Timer_information_to_follow = 1
    } T_q_sectiontimer ;
    typedef enum {
        Q_SLEEPSESSION_Ignore_session_establishment_order = 0 ,
        Q_SLEEPSESSION_Execute_session_establishment_order = 1
    } T_q_sleepsession ;
    typedef enum {
        Q_SRSTOP_Stop_if_in_SR_mode = 0 ,
        Q_SRSTOP_Go_if_in_SR_mode = 1
    } T_q_srstop ;
    int Q_SSCODE // 15 = Code_reserved_for_test_purposes
    ;
    typedef enum {
        Q_STATUS_Valid = 1 ,
        Q_STATUS_Unknown = 2
    } T_q_status ;
    typedef enum {
        Q_STOPLX_No_stop_required = 0 ,
        Q_STOPLX_Stop_required = 1
    } T_q_stoplx ;
    typedef enum {
        Q_SUITABILITY_Loading_gauge = 0 ,
        Q_SUITABILITY_Max_axle_load = 1 ,
        Q_SUITABILITY_Traction_system = 2
    } T_q_suitability ;
    typedef enum {
        Q_TEXT_Level_crossing_not_protected = 0 ,
        Q_TEXT_Acknowledgement = 1
    } T_q_text ;
    typedef enum {
        Q_TEXTCLASS_Auxiliary_Information = 0 ,
        Q_TEXTCLASS_Important_Information = 1
    } T_q_textclass ;
    typedef enum {
        Q_TEXTCONFIRM_No_confirmation_required = 0 ,
        Q_TEXTCONFIRM_Confirmation_required = 1 ,
        Q_TEXTCONFIRM_Confirmation_required_command_application_of_the_service_brake_when_display_end_condition_is_fulfilled_unless_the_text_has_already_been_acknowledged_by_the_driver = 2 ,
        Q_TEXTCONFIRM_Confirmation_required_command_application_of_the_emergency_brake_when_display_end_condition_is_fulfilled_unless_the_text_has_already_been_acknowledged_by_the_driver = 3
    } T_q_textconfirm ;
    typedef enum {
        Q_TEXTDISPLAY_No_display_as_soon_as__or__until_one_of_the_events_is_fulfilled = 0 ,
        Q_TEXTDISPLAY_Yes_display_as_soon_as__or__until_all_events_are_fulfilled = 1
    } T_q_textdisplay ;
    typedef enum {
        Q_TEXTREPORT_No_driver_acknowledgement_report_required = 0 ,
        Q_TEXTREPORT_Driver_acknowledgement_report_required = 1
    } T_q_textreport ;
    typedef enum {
        Q_TRACKINIT_No_initial_states_to_be_resumed_profile_to_follow = 0 ,
        Q_TRACKINIT_Empty_profile_initial_states_to_be_resumed = 1
    } T_q_trackinit ;
    typedef enum {
        Q_UPDOWN_Down_link_telegram = 0 ,
        Q_UPDOWN_Up_link_telegram = 1
    } T_q_updown ;
    typedef enum {
        Q_VBCO_Remove_the_Virtual_Balise_Cover = 0 ,
        Q_VBCO_Set_the_Virtual_Balise_Cover = 1
    } T_q_vbco ;
    int T_CYCLOC /* MinVal = 0, MaxVal = 254 */ // 255 = infinite
    ;
    int T_CYCRQST /* MinVal = 0, MaxVal = 254 */ // 255 = No_repetition
    ;
    int T_ENDTIMER /* MinVal = 0, MaxVal = 1022 */ // 1023 = infinite
    ;
    int T_LOA /* MinVal = 0, MaxVal = 1022 */ // 1023 = infinite
    ;
    int T_MAR /* MinVal = 0, MaxVal = 254 */ // 255 = _No_MA_request_triggering_with_regards_to_this_function
    ;
    int T_NVCONTACT /* MinVal = 0, MaxVal = 254 */ // 1111 1111 = T_NVCONTACT_infinite
    ;
    int T_NVOVTRP /* MinVal = 0, MaxVal = 255 */ ;
    int T_OL /* MinVal = 0, MaxVal = 1022 */ // 1023 = infinite
    ;
    int T_SECTIONTIMER /* MinVal = 0, MaxVal = 1022 */ // 1023 = infinite
    ;
    int T_TEXTDISPLAY /* MinVal = 0, MaxVal = 1022 */ // 1023 = Display_of_text_not_limited_by_time
    ;
    int T_TIMEOUTRQST /* MinVal = 0, MaxVal = 1022 */ // 1023 = _No_MA_request_triggering_with_regards_to_this_function
    ;
    float T_TRAIN /* MinVal = 0.0, MaxVal = 42949672.94 */ // 4294967295 = Unknown
    ;
    int T_VBC /* MinVal = 0, MaxVal = 255 */ ;
    int V_AXLELOAD /* MinVal = 0, MaxVal = 600 */ ;
    int V_DIFF /* MinVal = 0, MaxVal = 600 */ ;
    int V_LOA /* MinVal = 0, MaxVal = 600 */ ;
    int V_LX /* MinVal = 0, MaxVal = 600 */ ;
    int V_MAIN /* MinVal = 0, MaxVal = 600 */ // 0 = Means_trip_order
    ;
    int V_MAMODE /* MinVal = 0, MaxVal = 600 */ // 127 = Use_the_national_speed_value_of_the_required_mode
    ;
    int V_MAXTRAIN /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVALLOWOVTRP /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVKVINT /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVLIMSUPERV /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVONSIGHT /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVSUPOVTRP /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVREL /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVSHUNT /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVSTFF /* MinVal = 0, MaxVal = 600 */ ;
    int V_NVUNFIT /* MinVal = 0, MaxVal = 600 */ ;
    int V_RELEASEDP /* MinVal = 0, MaxVal = 600 */ // 126 = Use_onboard_calculated_release_speed
    // 127 = Use_national_value
    ;
    int V_RELEASEOL /* MinVal = 0, MaxVal = 600 */ // 126 = Use_onboard_calculated_release_speed
    // 127 = Use_national_value
    ;
    int V_REVERSE /* MinVal = 0, MaxVal = 600 */ ;
    int V_STATIC /* MinVal = 0, MaxVal = 600 */ // 127 = Non_numerical_value_telling_that_the_static_speed_profile_description_ends_at_D_STATIC(n)
    ;
    int V_TRAIN /* MinVal = 0, MaxVal = 600 */ ;
    int V_TSR /* MinVal = 0, MaxVal = 600 */ ;
    int X_TEXT ;
    # 26 "Adhesion_Factor.h" 2
    # 1 "/home/timon/Fraunhofer/openETCS/dataDictionary-working/Artifacts/Bitwalker/Locals.h" 1
    # 27 "Adhesion_Factor.h" 2
    # 1 "../Info_Record.h" 1
    
    /* =============================================================================
     Formalization of Subset-026-7 (Chapter 7: ERTMS/ETCS language)
     
     - Name: Subset-026-7 / TrackToTrain_Adhesion_Factor
     - Description: UNISIG SUBSET-026-7, ISSUE : 3.3.0, 3.5 ERTMS/ETCS language)
     - Copyright (c) Siemens AG, 2014, All Rights Reserved
     
     - Licensed under the EUPL V.1.1 ( http://joinup.ec.europa.eu/software/page/eupl/licence-eupl )
     - Gist URL: none
     - Cryptography: No
     - Author(s): SiemensRailAutomation
     
     Disclaimer:
     
     The use of this software is limited to NON-vital applications.
     It has NOT been developed for vital operation purposes and MUST NOT be used for applications
     which may cause harm to people, physical accidents or financial loss.
     
     THEREFORE, NO LIABILITY WILL BE GIVEN FOR SUCH AND ANY OTHER KIND OF USE.
     ============================================================================= */
    
    struct Info_Record
    {
        uint32_t v_TOccurence; // Zeitpunkt des Empfangs
        uint64_t v_DOccurrence; // Ort des Empfangs
        uint32_t vState; // Bearbeitungszustaende
    };
    # 28 "Adhesion_Factor.h" 2
    
    struct DATA_oETCS_TrackToTrain_Adhesion_Factor
    {
        
        struct Info_Record info;
        
        struct
        {
            // TransmissionMedia=Any
            // This packet is used when the trackside requests a change of the adhesion factor to be used in the brake model.
            // Packet Number = 71
            
            uint32_t NID_PACKET; // # 8
            T_q_dir Q_DIR ; // # 2
            uint32_t L_PACKET ; // # 13
            T_q_scale Q_SCALE ; // # 2
            uint32_t D_ADHESION ; // # 15
            uint32_t L_ADHESION ; // # 15
            T_m_adhesion M_ADHESION ; // # 1
        }
        packet; // Instanz der Sturkur mit dem content
    };
    
    // struct -> type
    typedef struct DATA_oETCS_TrackToTrain_Adhesion_Factor T_DATA_oETCS_TrackToTrain_Adhesion_Factor;
    // typ -> ptrtyp
    typedef T_DATA_oETCS_TrackToTrain_Adhesion_Factor* TP_DATA_oETCS_TrackToTrain_Adhesion_Factor;
    // declaration of variable of ptrtyp
    extern TP_DATA_oETCS_TrackToTrain_Adhesion_Factor oETCS_Packet_TrackToTrain_Adhesion_Factor;
    // instatiate this ptrtype variable like this: (get memory and fill memory)
    // TP_DATA_oETCS_TrackToTrain_Adhesion_Factor  oETCS_Packet_TrackToTrain_Adhesion_Factor = new(T_DATA_oETCS_TrackToTrain_Adhesion_Factor);
    // and now fill in the content to start with ...
    // Access variable like this: oETCS_Packet_TrackToTrain_Adhesion_Factor->...
    // maybe : memset(oETCS_Packet_TrackToTrain_Adhesion_Factor, 0, sizeof(T_DATA_oETCS_Packet_TrackToTrain_Adhesion_Factor));
    // for complete 0 content.
    
    // Decoder
    /*@
     requires \valid(oETCS);
     requires \valid(P_Telegram + (0..I_Cur_Dim-1));
     requires 8 * I_Cur_Dim <= UINT_MAX;
     requires Bit_Index <= 8 * I_Cur_Dim;
     
     assigns oETCS->packet.NID_PACKET;
     assigns oETCS->packet.Q_DIR;
     assigns oETCS->packet.L_PACKET;
     assigns oETCS->packet.Q_SCALE;
     assigns oETCS->packet.D_ADHESION;
     assigns oETCS->packet.L_ADHESION;
     assigns oETCS->packet.M_ADHESION;
     
     ensures \result == \old(Bit_Index) + 56;
     
     behavior error_case:
     
     assumes Bit_Index + 56 > 8 * I_Cur_Dim;
     
     behavior normal_case:
     
     assumes Bit_Index + 56 <= 8 * I_Cur_Dim;
     
     ensures EqualBits(P_Telegram, oETCS->packet.NID_PACKET, Bit_Index, 8);
     ensures NotSet(oETCS->packet.NID_PACKET, 64-8);
     
     ensures EqualBits(P_Telegram, oETCS->packet.Q_DIR, Bit_Index+8, 2);
     ensures NotSet(oETCS->packet.Q_DIR, 64-2);
     
     ensures EqualBits(P_Telegram, oETCS->packet.L_PACKET, Bit_Index+10, 13);
     ensures NotSet(oETCS->packet.L_PACKET, 64-13);
     
     ensures EqualBits(P_Telegram, oETCS->packet.Q_SCALE, Bit_Index+23, 2);
     ensures NotSet(oETCS->packet.Q_SCALE, 64-2);
     
     ensures EqualBits(P_Telegram, oETCS->packet.D_ADHESION, Bit_Index+25, 15);
     ensures NotSet(oETCS->packet.D_ADHESION, 64-15);
     
     ensures EqualBits(P_Telegram, oETCS->packet.L_ADHESION, Bit_Index+40, 15);
     ensures NotSet(oETCS->packet.L_ADHESION, 64-15);
     
     ensures EqualBits(P_Telegram, oETCS->packet.M_ADHESION, Bit_Index+55, 1);
     ensures NotSet(oETCS->packet.M_ADHESION, 64-1);
     
     complete behaviors;
     disjoint behaviors;
     
     */
    int TrackToTrain_Packet_071 (uint8_t* P_Telegram, uint32_t Bit_Index, uint32_t I_Cur_Dim, TP_DATA_oETCS_TrackToTrain_Adhesion_Factor oETCS);
    
    // Encoder
    /*@
     requires \valid(oETCS);
     requires \valid(P_Telegram + (0..I_Cur_Dim-1));
     requires 8 * I_Cur_Dim <= UINT_MAX;
     requires Bit_Index <= 8 * I_Cur_Dim;
     
     assigns P_Telegram + (0..I_Cur_Dim-1);
     
     ensures \result == \old(Bit_Index) + 56;
     
     behavior error_case:
     
     assumes Bit_Index + 56 > 8 * I_Cur_Dim;
     
     behavior normal_case:
     
     assumes Bit_Index + 56 <= 8 * I_Cur_Dim;
     
     ensures EqualBits(P_Telegram, oETCS->packet.NID_PACKET, Bit_Index, 8);
     ensures EqualBits(P_Telegram, oETCS->packet.Q_DIR, Bit_Index+8, 2);
     ensures EqualBits(P_Telegram, oETCS->packet.L_PACKET, Bit_Index+10, 13);
     ensures EqualBits(P_Telegram, oETCS->packet.Q_SCALE, Bit_Index+23, 2);
     ensures EqualBits(P_Telegram, oETCS->packet.D_ADHESION, Bit_Index+25, 15);
     ensures EqualBits(P_Telegram, oETCS->packet.L_ADHESION, Bit_Index+40, 15);
     ensures EqualBits(P_Telegram, oETCS->packet.M_ADHESION, Bit_Index+55, 1);
     
     complete behaviors;
     disjoint behaviors;
     
     */
    int TrackToTrain_Packet_071_Encoder (uint8_t* P_Telegram, uint32_t Bit_Index, uint32_t I_Cur_Dim, TP_DATA_oETCS_TrackToTrain_Adhesion_Factor oETCS);
    # 22 "Adhesion_Factor.c" 2
    
    int TrackToTrain_Packet_071 (uint8_t* P_Telegram, uint32_t Bit_Index, uint32_t I_Cur_Dim, TP_DATA_oETCS_TrackToTrain_Adhesion_Factor oETCS )
    {
        //    TP_DATA_oETCS_TrackToTrain_Adhesion_Factor oETCS  = (TP_DATA_oETCS_TrackToTrain_Adhesion_Factor)void_oETCS;
        T_Bitwalker_Incremental_Locals PeekLocals;
        Bitwalker_IncrementalWalker_Init(&PeekLocals, P_Telegram, I_Cur_Dim, Bit_Index);
        
        // TransmissionMedia=Any
        // Packet Number = 71
        oETCS->packet.NID_PACKET = (int) Bitwalker_IncrementalWalker_Peek_Next(&PeekLocals, 8);
        oETCS->packet.Q_DIR = (T_q_dir) Bitwalker_IncrementalWalker_Peek_Next(&PeekLocals, 2);
        oETCS->packet.L_PACKET = (int) Bitwalker_IncrementalWalker_Peek_Next(&PeekLocals, 13);
        oETCS->packet.Q_SCALE = (T_q_scale) Bitwalker_IncrementalWalker_Peek_Next(&PeekLocals, 2);
        oETCS->packet.D_ADHESION = (int) Bitwalker_IncrementalWalker_Peek_Next(&PeekLocals, 15);
        oETCS->packet.L_ADHESION = (int) Bitwalker_IncrementalWalker_Peek_Next(&PeekLocals, 15);
        oETCS->packet.M_ADHESION = (T_m_adhesion) Bitwalker_IncrementalWalker_Peek_Next(&PeekLocals, 1);
        return Bitwalker_IncrementalWalker_Peek_Finish (&PeekLocals);
        
    }
    // =======================
    
    
    int TrackToTrain_Packet_071_Encoder (uint8_t* P_Telegram, uint32_t Bit_Index, uint32_t I_Cur_Dim, TP_DATA_oETCS_TrackToTrain_Adhesion_Factor oETCS )
    {
        //    TP_DATA_oETCS_TrackToTrain_Adhesion_Factor oETCS  = (TP_DATA_oETCS_TrackToTrain_Adhesion_Factor)void_oETCS;
        T_Bitwalker_Incremental_Locals PokeLocals;
        Bitwalker_IncrementalWalker_Init(&PokeLocals, P_Telegram, I_Cur_Dim, Bit_Index);
        
        // TransmissionMedia=Any
        // Packet Number = 71
        Bitwalker_IncrementalWalker_Poke_Next(&PokeLocals, 8, oETCS->packet.NID_PACKET);
        Bitwalker_IncrementalWalker_Poke_Next(&PokeLocals, 2, oETCS->packet.Q_DIR);
        Bitwalker_IncrementalWalker_Poke_Next(&PokeLocals, 13, oETCS->packet.L_PACKET);
        Bitwalker_IncrementalWalker_Poke_Next(&PokeLocals, 2, oETCS->packet.Q_SCALE);
        Bitwalker_IncrementalWalker_Poke_Next(&PokeLocals, 15, oETCS->packet.D_ADHESION);
        Bitwalker_IncrementalWalker_Poke_Next(&PokeLocals, 15, oETCS->packet.L_ADHESION);
        Bitwalker_IncrementalWalker_Poke_Next(&PokeLocals, 1, oETCS->packet.M_ADHESION);
        return Bitwalker_IncrementalWalker_Poke_Finish (&PokeLocals);
        
    }
    // =======================
    
    // struct -> type
    typedef struct DATA_oETCS_Adhesion_Factor T_DATA_oETCS_Adhesion_Factor;
    // typ -> ptrtyp
    typedef T_DATA_oETCS_Adhesion_Factor* TP_DATA_oETCS_Adhesion_Factor;
    // declaration of variable of ptrtyp
    extern TP_DATA_oETCS_Adhesion_Factor oETCS_Packet_Adhesion_Factor;
    // instatiate this ptrtype variable like this: (get memory and fill memory)
    // TP_DATA_oETCS_Adhesion_Factor  oETCS_Packet_Adhesion_Factor = new(T_DATA_oETCS_Adhesion_Factor);
    // and now fill in the content to start with ...
    // Access variable like this: oETCS_Packet_Adhesion_Factor->...
    // maybe : memset(oETCS_Packet_Adhesion_Factor, 0, sizeof(T_DATA_oETCS_Packet_Adhesion_Factor));
    // for complete 0 content.
    c file icon foo.c (97,160 bytes) 2014-09-12 15:34 +

-Relationships
+Relationships

-Notes

~0005453

signoles (manager)

Thanks for your report. This crash is actually already fixed in the current development version.

With the current version, you get the following error message. It means that an assigns clause about P_Telegram+(0 .. I_Cur_Dim-1) is probably missing in one of your specifications (or there is an issue with your postcondition). I actually add such an assigns in your code, and now I get the same error message in another place of your code... I let you debug your spec forward :).

=====
Adhesion_Factor.h:91:[wp] user error: Non-assignable term (P_Telegram+(0 .. I_Cur_Dim-1))
[kernel] Plug-in wp aborted: invalid user input.
=====

~0005454

virgile (developer)

To complete Julien's answer:

- the error is not due to a missing assigns, but to an incorrect assigns: in your TrackToTrain_Packet_071_Encoder function, the assigns clause should read

    assigns P_Telegram[0 .. I_Cur_Dim-1];

Indeed, you want to assigns the cells of the array (assigns p means that you might modify the value of p, not the one of *p). As a matter of fact, this error ought to be reported by the kernel instead of the WP, as this is a syntactic error: arguments of assigns clause must be lvalues.

With this change, wp runs fine on your file, with 95/161 goals proved.
+Notes

-Issue History
Date Modified Username Field Change
2014-09-12 15:34 lapawczykt New Issue
2014-09-12 15:34 lapawczykt Status new => assigned
2014-09-12 15:34 lapawczykt Assigned To => correnson
2014-09-12 15:34 lapawczykt File Added: foo.c
2014-09-12 16:06 signoles Note Added: 0005453
2014-09-12 16:06 signoles Status assigned => resolved
2014-09-12 16:06 signoles Resolution open => fixed
2014-09-12 16:57 virgile Note Added: 0005454
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed
+Issue History