Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000550Frama-CPlug-in > occurrencepublic2010-07-28 17:162014-02-12 16:55
Reporterboris 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000550: Selecting "occurrence" crashes Frama-C
DescriptionMy binary search example crashes Frama-C if I right-click on some variable, eg low, and select "occurrence".
Additional InformationThe full backtrace is:
Raised at file "src/kernel/globals.ml", line 492, characters 10-95
Called from file "src/value/eval.ml", line 5154, characters 22-44
Re-raised at file "src/value/eval.ml", line 5169, characters 50-53
Called from file "src/project/computation.ml", line 914, characters 2-6
Re-raised at file "src/project/computation.ml", line 918, characters 8-11
Called from file "camlinternalOO.ml", line 374, characters 12-17
Called from file "camlinternalOO.ml", line 384, characters 24-40
Called from file "src/project/computation.ml", line 914, characters 2-6
Re-raised at file "src/project/computation.ml", line 918, characters 8-11
Called from file "src/occurrence/register.ml", line 152, characters 2-12
Called from file "src/kernel/journal.ml", line 323, characters 15-26
Re-raised at file "src/kernel/journal.ml", line 338, characters 14-15
Called from file "src/occurrence/register_gui.ml", line 37, characters 9-32
Called from file "src/lib/extlib.ml", line 176, characters 12-15
Re-raised at file "src/lib/extlib.ml", line 181, characters 10-11
Called from file "src/gui/gtk_helper.ml", line 533, characters 8-385

Unexpected error (Globals.No_such_entry_point("Could not find entry point: main")).
Please report as 'crash' at http://bts.frama-c.com [^]
TagsNo tags attached.
Attached Filesc file icon binary-search.c [^] (1,085 bytes) 2010-07-28 17:16 [Show Content]

- Relationships

-  Notes
(0001021)
signoles (manager)
2010-07-28 18:21

sure that's a bug.
You have to set kernel parameter "-main" to "binary_search" though.

- Issue History
Date Modified Username Field Change
2010-07-28 17:16 boris New Issue
2010-07-28 17:16 boris Status new => assigned
2010-07-28 17:16 boris Assigned To => signoles
2010-07-28 17:16 boris File Added: binary-search.c
2010-07-28 18:21 signoles Note Added: 0001021
2010-07-28 18:21 signoles Status assigned => acknowledged
2010-08-17 10:42 svn Checkin
2010-08-17 10:42 svn Status acknowledged => resolved
2010-08-17 10:42 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker