2021-03-03 03:44 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001790Frama-CPlug-in > jessiepublic2016-06-21 14:08
Reporterjohan 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSLinuxOS VersionDebian Jessie
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0001790: Crash when running "frama-c -jessie -jessie-atp=gui reduce.c"
DescriptionRunning "frama-c -jessie -jessie-atp=gui" on a simpler file works, but on the attached file, it produces an ml backtrace and asks me to report it as a crash to the BTS.
Steps To ReproduceRun "frama-c -jessie -jessie-atp=gui reduce.c" with the attached file reduce.c
Additional InformationThe -enable-journal option, which the bug reporting guidelines encourage me to use, only tells me user "error: option `-enable-journal' is unknown."


Full output:
$ frama-c -jessie -jessie-atp=gui reduce.c
[kernel] preprocessing with "gcc -C -E -I. -dD reduce.c"
[jessie] Starting Jessie translation
[kernel] Current source was: reduce.c:15
         The full backtrace is:
         Raised at file "norm.ml", line 769, characters 52-64
         Called from file "norm.ml", line 772, characters 47-69
         Called from file "list.ml", line 55, characters 20-23
         Called from file "norm.ml", line 788, characters 43-62
         Called from file "src/kernel/visitor.ml", line 162, characters 14-30
         Called from file "src/kernel/visitor.ml", line 384, characters 21-46
         Called from file "list.ml", line 66, characters 22-25
         Called from file "src/kernel/visitor.ml", line 382, characters 8-398
         Called from file "src/kernel/visitor.ml", line 583, characters 29-45
         Called from file "src/kernel/visitor.ml", line 784, characters 6-21
         Called from file "cil/src/cil.ml", line 3280, characters 5-53
         Called from file "cil/src/cil.ml", line 5881, characters 17-37
         Called from file "cil/src/cil.ml", line 5888, characters 3-20
         Called from file "cil/src/cil.ml", line 1858, characters 21-41
         Called from file "cil/src/cil.ml", line 5905, characters 15-39
         Called from file "norm.ml", line 1875, characters 2-27
         Called from file "register.ml", line 159, characters 4-23
         Called from file "register.ml", line 327, characters 6-12
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 37, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
         
         Unexpected error (File "norm.ml", line 769, characters 52-58: Assertion failed).
         Please report as 'crash' at http://bts.frama-c.com/.
         Your Frama-C version is Neon-20140301.
         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
TagsNo tags attached.
Attached Files
  • c file icon reduce.c (646 bytes) 2014-05-29 07:12 -
    /*@predicate descending(unsigned N, unsigned *tab) = \valid(tab+(0..N-1)) 
      && \forall unsigned r1, unsigned r2; 0 <= r1 <= r2 < N ==> tab[r1] >= tab[r2];
    
      @predicate reduced(unsigned n, unsigned *orig, unsigned *red) = 
      descending(n, orig) && 
      descending(n, red) && 
      \forall unsigned r; 0 <= r < n ==> red[r] == orig[r] - orig[n-1];
     */
    
    /*@ requires descending(n, tab);
      @ terminates \true;
      @ assigns tab+(0..n-1);
      @ ensures reduced(n, \old(tab), \result);
     */
    unsigned *reduce(unsigned n, unsigned *tab)
    {
        unsigned r;
        for (r = 0; r<n; r++)
        {
    	tab[r] -= tab[n-1];
        }
        return tab;
    }
    
    int main()
    {
        return 0;
    }
    
    c file icon reduce.c (646 bytes) 2014-05-29 07:12 +

-Relationships
+Relationships

-Notes

~0005170

yakobowski (manager)

Hi,

Thanks for noticing the problem with -journal-enable/-enable-journal in the guidelines. This is now fixed.

Although Jessie should not have crashed, the problem you encounter is actually in your specification. You should write 'assigns tab[0 .. n-1]' (or equivalently
'assigns *(tab+(0 .. n-1))', not 'assigns tab+(0 .. n-1)'

~0005174

johan (reporter)

Thanks for the quick reply, which solves the problem I had.

I expected that my specification was incorrect, as I am a beginner and I do not expect a crash for a correct test-case that is as simple as mine.

Thanks again.

~0006154

yakobowski (manager)

Fix committed to master branch.
+Notes

-Issue History
Date Modified Username Field Change
2014-05-29 07:12 johan New Issue
2014-05-29 07:12 johan Status new => assigned
2014-05-29 07:12 johan Assigned To => cmarche
2014-05-29 07:12 johan File Added: reduce.c
2014-05-29 11:17 yakobowski Note Added: 0005170
2014-05-29 17:45 johan Note Added: 0005174
2015-10-23 15:26 yakobowski Assigned To cmarche => yakobowski
2016-02-09 16:21 yakobowski Source_changeset_attached => framac master 9e13dd98
2016-02-09 16:21 yakobowski Note Added: 0006154
2016-02-09 16:21 yakobowski Status assigned => resolved
2016-02-09 16:21 yakobowski Resolution open => fixed
2016-06-21 14:08 signoles Fixed in Version => Frama-C Aluminium
2016-06-21 14:08 signoles Status resolved => closed
+Issue History