[WP] Unexpected error (Wp__NormAtLabels.LabelError(_))
Steps to reproduce the issue
git clone https://github.com/yrashk/clam
cd clam && ./test wp
Expected behaviour
Test to complete. It was last observed to work with 22.0
Actual behaviour
[kernel] Parsing clam.h (with preprocessing)
[rte:annot] annotating function clam_match_alpha_char
[rte:annot] annotating function clam_match_alphanumeric_char
[rte:annot] annotating function clam_match_anychar
[rte:annot] annotating function clam_match_at_least_n_chars
[rte:annot] annotating function clam_match_char
[rte:annot] annotating function clam_match_chars
[rte:annot] annotating function clam_match_chars_to_end
[rte:annot] annotating function clam_match_end
[rte:annot] annotating function clam_match_lowercase_char
[rte:annot] annotating function clam_match_numeric10_char
[rte:annot] annotating function clam_match_numeric16_char
[rte:annot] annotating function clam_match_posix_flags
[rte:annot] annotating function clam_match_posix_long_option
[rte:annot] annotating function clam_match_posix_option
[rte:annot] annotating function clam_match_posix_terminate_options
[rte:annot] annotating function clam_match_signed_integer10
[rte:annot] annotating function clam_match_unsigned_integer10
[rte:annot] annotating function clam_match_uppercase_char
[rte:annot] annotating function clam_match_windows_long_switch
[rte:annot] annotating function clam_match_windows_switch
[kernel] Current source was: clam.h:513
The full backtrace is:
Raised at Wp__NormAtLabels.labels_fct_pre in file "src/plugins/wp/normAtLabels.ml", line 136, characters 9-29
Called from Wp__NormAtLabels.norm_at#vterm.post.normalize in file "src/plugins/wp/normAtLabels.ml", line 82, characters 30-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Wp__NormAtLabels.norm_at#vterm.post in file "src/plugins/wp/normAtLabels.ml", line 83, characters 29-54
Called from Frama_c_kernel__Cil.visitCilTerm in file "src/kernel_services/ast_queries/cil.ml", line 1417, characters 12-63
Called from Frama_c_kernel__Cil.childrenPredicateNode.vTerm in file "src/kernel_services/ast_queries/cil.ml" (inlined), line 1799, characters 16-34
Called from Frama_c_kernel__Cil.childrenPredicateNode in file "src/kernel_services/ast_queries/cil.ml", line 1810, characters 14-22
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicate in file "src/kernel_services/ast_queries/cil.ml", line 1793, characters 16-56
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicateNode.vPred in file "src/kernel_services/ast_queries/cil.ml" (inlined), line 1797, characters 16-39
Called from Frama_c_kernel__Cil.childrenPredicateNode in file "src/kernel_services/ast_queries/cil.ml", line 1817, characters 14-22
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicate in file "src/kernel_services/ast_queries/cil.ml", line 1793, characters 16-56
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicateNode.vPred in file "src/kernel_services/ast_queries/cil.ml" (inlined), line 1797, characters 16-39
Called from Frama_c_kernel__Cil.childrenPredicateNode in file "src/kernel_services/ast_queries/cil.ml", line 1834, characters 14-22
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicate in file "src/kernel_services/ast_queries/cil.ml", line 1793, characters 16-56
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Visitor.visitFramacPredicate in file "src/kernel_services/visitors/visitor.ml", line 978, characters 11-48
Called from Wp__CfgAnnot.normalize_pre in file "src/plugins/wp/cfgAnnot.ml", line 80, characters 14-60
Called from Wp__CfgAnnot.CallContract.compile.add in file "src/plugins/wp/cfgAnnot.ml", line 338, characters 30-33
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Wp__CfgAnnot.CallContract.compile.(fun) in file "src/plugins/wp/cfgAnnot.ml", line 348, characters 12-59
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Wp__CfgAnnot.CallContract.compile in file "src/plugins/wp/cfgAnnot.ml", line 341, characters 8-671
Called from Wp__WpContext.Static.memoize in file "src/plugins/wp/wpContext.ml", line 447, characters 14-17
Called from Wp__WpContext.StaticGenerator.get in file "src/plugins/wp/wpContext.ml" (inlined), line 510, characters 12-31
Called from Wp__CfgAnnot.get_call_contract in file "src/plugins/wp/cfgAnnot.ml", line 372, characters 11-30
Called from Wp__CfgCalculus.Make.call in file "src/plugins/wp/cfgCalculus.ml", line 365, characters 12-52
Called from Wp__CfgCalculus.Make.stmt in file "src/plugins/wp/cfgCalculus.ml", line 233, characters 8-23
Re-raised at Wp__CfgCalculus.Make.stmt in file "src/plugins/wp/cfgCalculus.ml", line 237, characters 30-39
Called from Wp__CfgCalculus.Make.wp in file "src/plugins/wp/cfgCalculus.ml", line 214, characters 20-32
Called from Wp__CfgCalculus.Make.transition in file "src/plugins/wp/cfgCalculus.ml", line 305, characters 12-22
Called from Wp__CfgCalculus.Make.wp in file "src/plugins/wp/cfgCalculus.ml", line 213, characters 18-34
Called from Wp__CfgCalculus.Make.compute in file "src/plugins/wp/cfgCalculus.ml", line 544, characters 6-61
Called from Wp__CfgGenerator.Make.compute.(fun) in file "src/plugins/wp/cfgGenerator.ml", line 235, characters 30-53
Called from Wp__WpContext.on_context in file "src/plugins/wp/wpContext.ml", line 139, characters 17-20
Re-raised at Wp__WpContext.on_context in file "src/plugins/wp/wpContext.ml", line 146, characters 4-13
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Stdlib__Map.Make.iter in file "map.ml", line 297, characters 20-25
Called from Stdlib__Map.Make.iter in file "map.ml", line 297, characters 10-18
Called from Wp__CfgGenerator.Make.compute in file "src/plugins/wp/cfgGenerator.ml", line 219, characters 6-1023
Called from Wp__Register.cmdline_run in file "src/plugins/wp/register.ml", line 750, characters 20-61
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 14-17
Re-raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_boot__Boot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 880, characters 18-64
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (Wp__NormAtLabels.LabelError(_)).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.1 (Iron).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 26.1
- Plug-in used: WP
- OS name: macOS
- OS version: 13.3.1