Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #261

Closed
Open
Created Jul 04, 2018 by mantis-gitlab-migration@mantis-gitlab-migration

WP: internal error: only the kernel should set the status of property assumes

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking