--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on June 2019 ---
On 16/06/2019 17:12, Roderick Chapman wrote: > On 15/06/2019 11:15, Gerlach, Jens wrote: >> The code of the examples and the various logic functions and >> predicates can be found under >> >> https://github.com/fraunhoferfokus/acsl-by-example > > OK..got it... you define a predicate called "Empty" and use that in > the "ensures" clause of the "stack_empty" function... which can then > be used in the preconditions of other functions... OK... I've got that far, but now I find that my code crashes the wp plugin somewhere. I will try to reproduce a smaller code sample to submit a bug report. For what it's worth, I get: $ frama-c -wp log.h [kernel] Parsing log.h (with preprocessing) [kernel] Current source was: log.h:49  The full backtrace is:  Raised at file "src/kernel_services/ast_queries/cil.ml", line 6472, characters 5-17  Called from file "src/kernel_services/ast_queries/cil.ml", line 2367, characters 12-44  Called from file "src/kernel_services/ast_queries/cil.ml", line 2250, characters 21-41  Called from file "src/kernel_services/ast_queries/cil.ml", line 2363, characters 12-63  Called from file "src/plugins/wp/Cvalues.ml", line 68, characters 10-34  Called from file "src/plugins/wp/LogicSemantics.ml", line 640, characters 13-38  Called from file "src/plugins/wp/Warning.ml", line 145, characters 6-10  Called from file "src/plugins/wp/LogicSemantics.ml", line 980, characters 12-32  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 35-46  Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35  Called from file "src/plugins/wp/LogicSemantics.ml", line 731, characters 17-30  Called from file "src/plugins/wp/Warning.ml", line 145, characters 6-10  Called from file "src/plugins/wp/LogicSemantics.ml", line 980, characters 12-32  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 35-46  Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35  Called from file "src/plugins/wp/LogicSemantics.ml", line 142, characters 10-23  Called from file "src/plugins/wp/LogicCompiler.ml", line 399, characters 21-32  Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17  Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48  Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17  Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48  Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17  Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48  Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17  Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48  Called from file "src/plugins/wp/LogicCompiler.ml", line 595, characters 17-70  Called from file "src/plugins/wp/LogicCompiler.ml", line 611, characters 21-54  Called from file "src/plugins/wp/Model.ml", line 270, characters 14-17  Called from file "src/plugins/wp/Model.ml" (inlined), line 277, characters 11-24  Called from file "src/plugins/wp/LogicCompiler.ml", line 733, characters 25-62  Called from file "list.ml", line 85, characters 12-15  Called from file "src/plugins/wp/LogicCompiler.ml", line 747, characters 6-66  Called from file "src/plugins/wp/LogicCompiler.ml", line 759, characters 26-53  Called from file "src/plugins/wp/cfgWP.ml", line 1351, characters 31-42  Called from file "map.ml", line 270, characters 20-25  Called from file "map.ml", line 270, characters 10-18  Called from file "map.ml", line 270, characters 10-18  Called from file "map.ml", line 270, characters 10-18  Called from file "map.ml", line 270, characters 10-18  Called from file "src/plugins/wp/cfgWP.ml", line 1435, characters 19-59  Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17  Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48  Called from file "src/plugins/wp/Context.ml" (inlined), line 73, characters 21-47  Called from file "src/plugins/wp/Model.ml" (inlined), line 127, characters 21-45  Called from file "src/plugins/wp/Model.ml" (inlined), line 129, characters 18-36  Called from file "src/plugins/wp/cfgWP.ml", line 1433, characters 14-202  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 19-28  Called from file "src/plugins/wp/Model.ml" (inlined), line 126, characters 19-36  Called from file "src/plugins/wp/cfgWP.ml", line 1431, characters 10-1023  Called from file "src/plugins/wp/register.ml", line 686, characters 15-40  Called from file "src/libraries/stdlib/extlib.ml", line 332, characters 14-17  Re-raised at file "src/libraries/stdlib/extlib.ml", line 332, characters 41-48  Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12  Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-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  Unexpected error (File "src/kernel_services/ast_queries/cil.ml", line 6472, characters 5-11: Assertion failed).  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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190617/f4782ea5/attachment.html>