| Description | Running 'frama-c -wp part.c whole.c' on the attached files causes the follwoing crash:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing part.c (with preprocessing)
[kernel] Parsing whole.c (with preprocessing)
[wp] warning: Missing RTE guards
[kernel] Current source was: whole.c:12
The full backtrace is:
Raised at file "map.ml", line 117, characters 16-25
Called from file "list.ml", line 55, characters 20-23
Called from file "src/plugins/wp/LogicCompiler.ml", line 772, characters 17-61
Called from file "src/plugins/wp/Warning.ml", line 139, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 853, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 41-46
Called from file "src/plugins/wp/Warning.ml", line 155, characters 14-18
Called from file "src/plugins/wp/cfgWP.ml", line 461, characters 23-135
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "list.ml", line 84, characters 24-34
Called from file "src/plugins/wp/calculus.ml", line 339, characters 22-62
Called from file "src/plugins/wp/calculus.ml", line 343, characters 23-45
Called from file "src/plugins/wp/calculus.ml", line 647, characters 20-43
Called from file "src/plugins/wp/calculus.ml", line 606, characters 19-40
Called from file "src/plugins/wp/calculus.ml", line 757, characters 40-59
Called from file "set.ml", line 305, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/calculus.ml", line 757, characters 4-64
Called from file "src/plugins/wp/calculus.ml", line 793, characters 19-51
Called from file "src/plugins/wp/cfgWP.ml", line 1468, characters 43-66
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/cfgWP.ml", line 1456, characters 14-957
Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 25-28
Called from file "src/plugins/wp/Model.ml", line 126, characters 19-36
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
The problem disappears if:
* the source file order is exchanged on the command line,
* the overloaded predicate 'Bnd(integer n)' in while.c:5 is renamed e.g. to 'Bnd2',
* the trivial 'ensures' clause is removed in whole.c:10, or
* the 'requires' clause in whole.c:9 is changed to 'Bnd(1,(int)0)', i.e. 'Bnd' is inlined.
|
part.c [^] (97 bytes) 2017-07-31 13:14 [Show Content]
Relationships 
Relationships