Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Planning hierarchy
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • 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
  • #2117

Closed
Open
Created Aug 12, 2011 by mantis-gitlab-migration@mantis-gitlab-migration

Wp rises an error in if you use struct and long long type, with wp-rte option

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


Id Project Category View Due Date Updated
ID0000925 Frama-C Plug-in > wp public 2011-08-12 2011-10-10
Reporter jessie_user Assigned To correnson Resolution fixed
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Carbon-20101202-beta2 Target Version - Fixed in Version Frama-C Nitrogen-20111001

Description :

Following command with -wp-rte option rises an error.

frama-c -wp -wp-rte -wp-out wp_longlong test_wp_longlong.c

Output:

frama-c -wp -wp-rte -wp-out wp_longlong test_wp_longlong.c [kernel] preprocessing with "gcc -C -E -I. test_wp_longlong.c" [rte] annotating function add [kernel] The full backtrace is: Raised at file "src/kernel/command.ml", line 42, characters 10-13 Called from file "src/wp/cfgProof.ml", line 125, characters 4-118 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "src/wp/cfgProof.ml", line 223, characters 1-607 Called from file "src/wp/register.ml", line 322, characters 41-57 Called from file "src/wp/register.ml", line 464, characters 3-32 Called from file "src/wp/register.ml", line 533, characters 8-20 Called from file "src/wp/register.ml", line 570, characters 4-18 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 660, characters 2-9 Called from file "src/kernel/cmdline.ml", line 173, characters 4-8

     Unexpected error (Failure("int_of_string")).
     Please report as 'crash' at http://bts.frama-c.com/
     Note that a backtrace alone often does not have 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

Without wp-rte Option ok: frama-c -wp -wp-out wp_longlong test_wp_longlong.c [kernel] preprocessing with "gcc -C -E -I. test_wp_longlong.c" [wp] warning: Missing RTE guards

If you use int type in INTEGER32 structure, then its ok.

Additional Information :

struct INTEGER32 { // int value; // Ok long long value; // Fails };

typedef struct INTEGER32 int32;

/*@ requires \valid(x) && \valid(y);

/ void add (int32 x, int32* y){ int32 erg; erg.value = x->value + y->value; }

Attachments

  • test_wp_longlong.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking