Actions
Bug #10026
openpostaction_term: unexpected term: &v_n_1
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
No data to display
Actions