Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:39 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001056Frama-CKernel > ACSL implementationpublic2011-12-21 10:462014-02-12 16:58
ReporterChitman 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
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 - 
    

typedef unsigned short int Action;
typedef Action* MultiSetType;


void multiset_difference(MultiSetType mm1, MultiSetType mm2);

/*@ axiomatic IntMultiSetTheory {
  @ type int_multiset;
  @
  @ logic int_multiset empty_int_multiset;
  @ logic int_multiset add_int_multiset(int_multiset s, Action i);
  @ logic integer contains(int_multiset s, integer i);

  @
  @ axiom contains_empty_multiset:
  @  \forall Action i; 
  @         contains(empty_int_multiset, i) == 0;
  @
  @
  @ axiom add_int_multiset_trans:
  @  \forall int_multiset s, Action i, Action j; 
  @    add_int_multiset(add_int_multiset(s,i),j) == 
  @                           add_int_multiset(add_int_multiset(s,j),i); 
  @
  @ 
  @ axiom contains_add_multiset:
  @  \forall int_multiset s, Action i; contains(add_int_multiset(s,i),i) == contains(s,i) + 1;
  @
  @  
  @ axiom contains3_multiset:
  @  \forall int_multiset s, Action i, Action j; 
  @                  (i != j) 
  @               ==>  
  @                    (contains(add_int_multiset(s,i),j) == contains(s,j) );
  @ 
  @
  @
  @
  @	lemma test:
  @		\forall integer c, int_multiset s;
  @			
  @				(\forall integer i; (sizeof(Action) <= i < sizeof(c))
  @					==> (contains(s, i) == 0) );
  @ }
  @*/
    ? file icon multiset_diff.h (1,242 bytes) 2011-12-21 10:46 +
  • c file icon multiset_diff.c (149 bytes) 2011-12-23 14:07 - 
    #include <stdlib.h>
#include "multiset_diff.h"/*Added*/


void multiset_difference(MultiSetType/*MultiSet*/ mm1, MultiSetType/*MultiSet*/ mm2)
{

}
    c file icon multiset_diff.c (149 bytes) 2011-12-23 14:07 +

-Relationships
+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.
+Notes

-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
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
2013-12-19 01:11 Source_changeset_attached => framac master 6a590b7a
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 6a590b7a
2014-02-12 16:58 Note Added: 0004690
2014-02-12 16:58 Status closed => resolved
+Issue History