Project

General

Profile

Actions

Bug #9543

closed

Frama-C (CIL) dislikes large enumerators

Added by Evgeny Novikov over 5 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
Urgent
Start date:
03/14/2019
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

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
};

Frama-C (CIL) issues the following error:
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.


Files

fvtp.tar.gz (7.89 MB) fvtp.tar.gz Evgeny Novikov, 03/14/2019 10:35 AM

Related issues 1 (0 open1 closed)

Blocks Klever - Bug #6629: Used CIL is outdatedClosedEvgeny Novikov03/13/2019

Actions
Actions #1

Updated by Evgeny Novikov over 5 years ago

  • Blocks Bug #6629: Used CIL is outdated added
Actions #2

Updated by Mikhail Mandrykin over 5 years ago

  • Status changed from New to Resolved

I changed the list of integer kinds to choose from when parsing integer constants in GCC mode (-machdep gcc_x86_64) (2b0abc74), so this should now work. The relevant comment in the source says this treatment is different from some standard-compatible behavior, however GCC just says "warning: integer constant is so large that it is unsigned" for such constants.

Actions #3

Updated by Evgeny Novikov over 5 years ago

Thank you, it helps! Please, close the issue.

Actions #4

Updated by Mikhail Mandrykin over 5 years ago

  • Status changed from Resolved to Closed
Actions

Also available in: Atom PDF