GitLab

ID0002383: This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002383	Frama-C	Plug-in > wp	public	2018-07-04	2018-07-04

Reporter	evdenis	Assigned To	correnson	Resolution	unable to reproduce
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	Frama-C 17-Chlorine

Description :

Example:

int test(void)
{
        int a = 1;
        /*@ behavior ok:
                assumes a > 0;
                ensures \true;
         */
        return 3;
}

Command:

frama-c -wp test.c

Log:

[wp] [CFG] Goal test_stmt_ok_post : Valid (Unreachable)
[wp] [CFG] Goal test_stmt_ok_assume : Valid (Unreachable)
[kernel] failure: only the kernel should set the status of property assumes
                  a > 0
[kernel] Current source was: test.c:1
         The full backtrace is:
         Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 568, characters 24-31
         Called from file "src/kernel_services/plugin_entry_points/log.ml", line 939, characters 6-44
         Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
         Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 9-16
         Called from file "src/kernel_services/ast_data/property_status.ml", line 538, characters 4-109
         Called from file "src/kernel_services/ast_data/property_status.ml" (inlined), line 551, characters 42-80
         Called from file "src/plugins/wp/wpAnnot.ml", line 81, characters 4-71
         Called from file "list.ml", line 85, characters 12-15
         Called from file "list.ml", line 85, characters 12-15
         Called from file "src/plugins/wp/wpAnnot.ml", line 1243, characters 10-38
         Called from file "src/plugins/wp/wpAnnot.ml", line 1258, characters 12-28
         Called from file "src/plugins/wp/wpAnnot.ml", line 1271, characters 16-68
         Called from file "src/plugins/wp/Generator.ml", line 108, characters 4-67
         Called from file "map.ml", line 270, characters 20-25
         Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
         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 41-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 105, characters 6-15
         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

         Frama-C aborted: internal error.
         Please report as 'crash' at http://bts.frama-c.com/.

Attachments

• test.c