AstraVer Toolset » Deductive Verification Tools for Linux Kernel

For such the enumeration with "-machdep x86_64":

enum ldv_37266
{
  PERF_TXN_ELISION = 1,
  PERF_TXN_TRANSACTION = 2,
  PERF_TXN_SYNC = 4,
  PERF_TXN_ASYNC = 8,
  PERF_TXN_RETRY = 16,
  PERF_TXN_CONFLICT = 32,
  PERF_TXN_CAPACITY_WRITE = 64,
  PERF_TXN_CAPACITY_READ = 128,
  PERF_TXN_MAX = 256,
  PERF_TXN_ABORT_MASK = 18446744069414584320,
  PERF_TXN_ABORT_SHIFT = 32
};

Cannot represent the integer 18446744069414584320

Besides, I attach the complete set of input source file and here is the complete command:

toplevel.opt "-no-autoload-plugins" "-no-findlib" "-machdep" "x86_64" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-keep-logical-operators" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_client.abs-paths.trimmed.i" ".tmp_nfstrace.abs-paths.trimmed.i" ".tmp_dir.abs-paths.trimmed.i" ".tmp_inode.abs-paths.trimmed.i" ".tmp_direct.abs-paths.trimmed.i" ".tmp_file.abs-paths.trimmed.i" ".tmp_fscache-index.abs-paths.trimmed.i" ".tmp_namespace.abs-paths.trimmed.i" ".tmp_unlink.abs-paths.trimmed.i" ".tmp_sysctl.abs-paths.trimmed.i" ".tmp_read.abs-paths.trimmed.i" ".tmp_getroot.abs-paths.trimmed.i" ".tmp_super.abs-paths.trimmed.i" ".tmp_pagelist.abs-paths.trimmed.i" ".tmp_symlink.abs-paths.trimmed.i" ".tmp_fscache.abs-paths.trimmed.i" ".tmp_write.abs-paths.trimmed.i" ".tmp_mount_clnt.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "dd.abs-paths.trimmed.i" "spi.abs-paths.trimmed.i" "err.abs-paths.trimmed.i" "panic.abs-paths.trimmed.i" "common.abs-paths.trimmed.i" "slab.abs-paths.trimmed.i" "memory.abs-paths.trimmed.i" "gcc.abs-paths.trimmed.i" "nondet.abs-paths.trimmed.i" "reference memory.abs-paths.trimmed.i" "environment_model.abs-paths.trimmed.i" "spinlock.bk.abs-paths.trimmed.i" "bug kind funcs.trimmed.i" 

Old CIL processed this well.