Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>