Actions
Bug #10022
openinternal error: named literals bug
Start date:
12/31/2019
Due date:
% Done:
0%
Estimated time:
Detected in build:
svn
Platform:
Published in build:
Description
$ frama-c -av ghost_named_literals.c [kernel] Parsing ghost_named_literals.c (with preprocessing) [av] Starting AstraVer translation [av] ghost_named_literals.c:22:10: Failure: No matching literals found for proxy specification (variable proxy1) [kernel] Current source was: ghost_named_literals.c:22 The full backtrace is: Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 533, characters 24-31 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1099, characters 17-55 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 526, characters 9-23 Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 529, characters 9-16 Called from file "src/kernel_services/ast_queries/cil.ml", line 2238, characters 15-31 Called from file "src/kernel_services/ast_queries/cil.ml", line 3925, characters 28-57 Called from file "src/kernel_services/ast_queries/cil.ml", line 2277, characters 13-16 Called from file "src/kernel_services/ast_queries/cil.ml", line 2322, characters 24-57 Called from file "src/kernel_services/ast_queries/cil.ml", line 3865, characters 5-53 Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 6623, characters 17-37 Called from file "src/kernel_services/ast_queries/cil.ml", line 6628, characters 24-33 Called from file "src/kernel_services/ast_queries/cil.ml", line 6630, characters 3-20 Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41 Called from file "src/kernel_services/ast_queries/cil.ml", line 6647, characters 15-39 Called from file "common.ml", line 1904, characters 4-148 Called from file "rewrite.ml", line 2505, characters 2-8 Called from file "rewrite.ml" (inlined), line 2509, characters 14-25 Called from file "rewrite.ml", line 2548, characters 2-81 Called from file "register.ml", line 146, characters 2-22 Called from file "register.ml", line 303, characters 6-12 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8 Plug-in av aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is 18.0 (Argon). 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
Files
No data to display
Actions