Project

General

Profile

Bug #9543

Frama-C (CIL) dislikes large enumerators

Added by Evgeny Novikov 8 months ago. Updated 8 months 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

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

Actions

History

#1

Updated by Evgeny Novikov 8 months ago

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

Updated by Mikhail Mandrykin 8 months 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.

#3

Updated by Evgeny Novikov 8 months ago

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

#4

Updated by Mikhail Mandrykin 8 months ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF