Project

General

Profile

Actions

Bug #10022

open

internal error: named literals bug

Added by Denis Efremov about 4 years ago.

Status:
New
Priority:
Normal
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

ghost_named_literals.c (1.99 KB) ghost_named_literals.c Denis Efremov, 12/31/2019 12:47 AM

No data to display

Actions

Also available in: Atom PDF