"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
- Expand "repro.c" on the file panel.
- Click "Foo" on the file panel.
- Right-click the "ensures" annotation in the source panel.
- Click "Prove property by WP".
- On the toolbar, click the "Reparse source files, and replay analyses" button.
- Click "repro.c" on the file panel.
- Right-click the "ensures" annotation in the source panel.
- 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