Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001056Frama-CKernel > ACSL implementationpublic2011-12-21 10:462014-02-12 16:58
ReporterChitman 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001056: Frama-c fails when Starting Jessie Translation
DescriptionFull Stacktrace:

tester@ubuntu-fm:~/Desktop/iteration1/task2$ frama-c -jessie multiset_diff.c
[kernel] preprocessing with "gcc -C -E -I. -dD multiset_diff.c"
[jessie] Starting Jessie translation
multiset_diff.h:45:[jessie] failure: Unexpected failure.
                  Please submit bug report (Ref. "cil/src/cil.ml:7780:2").
[kernel] The full backtrace is:
         Raised at file "src/kernel/log.ml", line 507, characters 30-31
         Called from file "src/kernel/log.ml", line 501, characters 2-9
         Re-raised at file "src/kernel/log.ml", line 504, characters 8-9
         Called from file "src/type/type.ml", line 600, characters 39-44
         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 713, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 195, characters 4-8
         
         Plug-in jessie aborted because of internal error.
         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 [^]


------------------------

Pls see .h file in attach.

Additional InformationProblem lines:

  @ lemma test:
  @ \forall integer c, int_multiset s;
  @ (\forall integer i; (sizeof(Action) <= i < sizeof(c))
  @ ==> (contains(s, i) == 0) );
TagsNo tags attached.
Attached Files? file icon multiset_diff.h [^] (1,242 bytes) 2011-12-21 10:46 [Show Content]
c file icon multiset_diff.c [^] (149 bytes) 2011-12-23 14:07 [Show Content]

- Relationships

-  Notes
(0002564)
virgile (developer)
2012-01-03 09:36

I'm not too sure about the meaning of lemma test, but the issue is the following:
sizeof(c) should not be accepted by the kernel in the first place, as c as a purely logic type (integer), that does not have a defined size (sizeof is only defined over C types).
(0004690)

2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-12-21 10:46 Chitman New Issue
2011-12-21 10:46 Chitman Status new => assigned
2011-12-21 10:46 Chitman Assigned To => cmarche
2011-12-21 10:46 Chitman File Added: multiset_diff.h
2011-12-23 14:07 Chitman File Added: multiset_diff.c
2012-01-03 09:36 virgile Note Added: 0002564
2012-01-03 09:36 virgile Assigned To cmarche => virgile
2012-01-03 09:36 virgile Status assigned => confirmed
2012-01-03 09:36 virgile Category Plug-in > jessie => Kernel > ACSL implementation
2012-01-06 15:43 svn Checkin
2012-01-06 15:43 svn Status confirmed => resolved
2012-01-06 15:43 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:58 Note Added: 0004690
2014-02-12 16:58 Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker