Actions
Bug #9543
closedFrama-C (CIL) dislikes large enumerators
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
Updated by Evgeny Novikov over 5 years ago
- Blocks Bug #6629: Used CIL is outdated added
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.
Updated by Evgeny Novikov over 5 years ago
Thank you, it helps! Please, close the issue.
Updated by Mikhail Mandrykin over 5 years ago
- Status changed from Resolved to Closed
Actions