Project

General

Profile

Actions

Bug #10026

open

postaction_term: unexpected term: &v_n_1

Added by Denis Efremov about 4 years ago.

Status:
New
Priority:
Normal
Start date:
01/09/2020
Due date:
% Done:

0%

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

Description

$ frama-c -av hlist_add_head.c

[kernel] Parsing result/hlist_add_head.c (with preprocessing)
[av] Starting AstraVer translation
[av] Warning: \separated is not supported by AstraVer. This predicate will be ignored
[av] result/hlist_add_head.c:24:32: Failure: 
  postaction_term: unexpected term: &v_n_1
[kernel] Current source was: result/hlist_add_head.c:24
  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 "common.ml", line 1959, characters 22-25
  Called from file "common.ml" (inlined), line 2154, characters 42-45
  Called from file "common.ml", line 2164, characters 77-83
  Called from file "src/kernel_services/ast_queries/cil.ml", line 2370, characters 12-63
  Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 2774, characters 17-35
  Called from file "src/kernel_services/ast_queries/cil.ml", line 2786, characters 12-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 2768, characters 17-57
  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" (inlined), line 2772, characters 17-40
  Called from file "src/kernel_services/ast_queries/cil.ml", line 2821, characters 12-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 2768, characters 17-57
  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 2763, characters 11-34
  Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41
  Called from file "src/kernel_services/visitors/visitor.ml", line 196, characters 22-53
  Called from file "list.ml", line 117, characters 24-34
  Called from file "src/kernel_services/ast_data/annotations.ml", line 631, characters 8-27
  Called from file "hashtbl.ml", line 317, characters 23-40
  Called from file "hashtbl.ml", line 324, characters 14-35
  Re-raised at file "hashtbl.ml", line 330, characters 4-13
  Called from file "src/kernel_services/ast_data/annotations.ml", line 635, characters 4-57
  Called from file "src/kernel_services/visitors/visitor.ml", line 211, characters 10-67
  Called from file "src/kernel_services/visitors/visitor.ml", line 228, characters 8-253
  Called from file "src/kernel_services/visitors/visitor.ml", line 423, characters 21-41
  Called from file "list.ml", line 99, characters 22-25
  Called from file "src/kernel_services/visitors/visitor.ml", line 421, characters 8-398
  Called from file "src/kernel_services/visitors/visitor.ml", line 623, characters 38-54
  Called from file "src/kernel_services/visitors/visitor.ml", line 815, characters 6-21
  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 "rewrite.ml", line 2505, characters 2-8
  Called from file "norm.ml" (inlined), line 2056, characters 14-33
  Called from file "norm.ml", line 2072, characters 2-83
  Called from file "register.ml", line 153, characters 2-21
  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

Files

hlist_add_head.c (1.07 KB) hlist_add_head.c Denis Efremov, 01/09/2020 09:10 PM

No data to display

Actions

Also available in: Atom PDF