--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on June 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Help with using user-declared functions in preconditions



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>