2021-01-27 07:01 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000379Frama-CPlug-in > jessiepublic2012-09-21 11:25
Reporterkerstin 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000379: \separated
DescriptionHello,

we get a crash using the \separate clause in line 8 of the attached example.

Regards,

Kerstin
Additional Informationframa-c -jessie -jessie-why-opt="-exp goal" swap_range.c &

gwlan61:swap_ranges kerstin$ [kernel] preprocessing with "gcc -C -E -I. -dD swap_range.c"
[jessie] Starting Jessie translation
swap_range.c:8:[jessie] failure: Unexpected exception.
                  Please submit bug report (Ref. "Extlib.NotYetImplemented("Interp.pred Pseparated")").
[kernel] Plugin jessie aborted because of an internal error.
         Please report with 'crash' at http://bts.frama-c.com
TagsNo tags attached.
Attached Files
  • c file icon swap_range.c (997 bytes) 2010-01-21 16:15 -
    /*@
     predicate is_valid_int_range(int* a, int n) = (0 <= n) && \valid_range(a, 0, n-1);
     */
    
    /*@
     requires is_valid_int_range(a, n);
     requires is_valid_int_range(b, n);
     requires \separated(a+(0..n-1), b+(0..n-1));
     
     assigns a[0..n-1];
     assigns b[0..n-1];
     
     ensures \forall int k; 0 <= k < n ==> a[k] == \old(b[k]);
     ensures \forall int k; 0 <= k < n ==> b[k] == \old(a[k]);
     */
    void swap_ranges(int* a, int n, int* b)
    {
      /*@
       loop assigns a[0..i-1];
       loop assigns b[0..i-1];
       
       loop invariant 0 <= i <= n;
       loop   variant n-i;
       
       loop invariant \forall int k; 0 <= k < i ==> 
                       a[k] == \at(b[k],Pre);
       loop invariant \forall int k; 0 <= k < i ==> 
                       b[k] == \at(a[k],Pre);
       */
      for (int i = 0; i < n; i++)
        swap(&a[i], &b[i]);
    }
    
    /*@
     requires \valid(p);
     requires \valid(q);
     
     assigns *p;
     assigns *q;
     
     ensures *p == \old(*q);
     ensures *q == \old(*p);
     */
    void swap(int* p, int* q)
    {
      int const save = *p;
      *p = *q;
      *q = save;
    }
    
    c file icon swap_range.c (997 bytes) 2010-01-21 16:15 +

-Relationships
has duplicate 0001002closedcmarche weak feature request for \separated under why-2.30 
+Relationships

-Notes

~0003090

yakobowski (manager)

Jessie ignoring \separated clauses would be great. This would make comparisons between Jessie and WP much easier, as the same specs could be used for both.

~0003478

virgile (developer)

Suggestion of note #3090 is now implemented: Jessie will only warn when it encounters a \separated (once per program) and just ignore it.
+Notes

-Issue History
Date Modified Username Field Change
2010-01-21 16:15 kerstin New Issue
2010-01-21 16:15 kerstin Status new => assigned
2010-01-21 16:15 kerstin Assigned To => cmarche
2010-01-21 16:15 kerstin File Added: swap_range.c
2012-06-10 13:25 yakobowski Note Added: 0003090
2012-09-21 11:25 virgile Note Added: 0003478
2012-10-30 20:25 yakobowski Relationship added has duplicate 0001002
+Issue History