Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #398
Closed
Open
Issue created Jul 30, 2016 by mantis-gitlab-migration@mantis-gitlab-migration

"Builtin already registered" after Reparse

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


Id Project Category View Due Date Updated
ID0002242 Frama-C Plug-in > wp public 2016-07-30 2016-12-05
Reporter khar Assigned To bobot Resolution fixed
Priority normal Severity crash Reproducibility always
Platform - OS lubuntu OS Version -
Product Version Frama-C Aluminium Target Version - Fixed in Version -

Description :

When using frama-c-gui to analyze code that uses arrays or pointers to structs, after a Reparse, the GUI fails to perform further analysis.

Additional Information :

Step 2 (selecting the function "Foo" rather than the file "repro.c") is needed to work around a possibly unrelated bug where the source viewer doesn't update properly after a Reparse. To reproduce that bug, simply click "repro.c" instead of "Foo" in step 2.

Steps To Reproduce :

$ cat repro.c: //@ ensures foo[1] == 1; void Foo(int* foo) { foo[1] = 1; }

$ frama-c-gui repro.c

  1. Expand "repro.c" on the file panel.
  2. Click "Foo" on the file panel.
  3. Right-click the "ensures" annotation in the source panel.
  4. Click "Prove property by WP".
  5. On the toolbar, click the "Reparse source files, and replay analyses" button.
  6. Click "repro.c" on the file panel.
  7. Right-click the "ensures" annotation in the source panel.
  8. Click "Prove property by WP".

Results: an error dialog with the following text:

Current source was: repro.c:2 The full backtrace is: Raised at file "hashtbl.ml", line 328, characters 23-32 Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38

Unexpected error (Failure("Builtin already registered for 'shift_sint32'")). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Aluminium-20160501. 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

Attachments

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