Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000029Frama-CPlug-in > jessiepublic2009-04-07 14:072009-06-23 18:03
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000029: Lithium fool the tool
Description[bug 7117 from old bts, reported by Christoph Weber]
Hello, unfortunatly I dont have time to track the bug down, so I will post the message I posted in the discussion list:

Hello again in the new year,
 
today I am trying to modify an implementation and still concurr with the function contract.
 
Therefore following code first:
/*@
    requires 0 <= length;
    requires \valid_range (a, 0, length-1);
    requires \valid_range (b, 0, length-1);
 
    assigns \nothing;
    
    behavior equal:
        ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> a[i] == b[i]);
    behavior not_equal:
        ensures \result == 0 <==> (\exists integer i; 0 <= i < length && a[i] != b[i]);
*/
int equal_array (int* a, int length, int* b )
{
    int index_a = 0;
    int index_b = 0;
    /*@
        loop invariant 0 <= index_a <= length;
        loop invariant 0 <= index_b <= length;
        loop invariant index_a == index_b;
 
        loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == b[k];
 
    */
    while ( index_a != length )
    {
        if (a[index_a] != b[index_b])
            return 0;
        ++index_a;
       ++index_b;
     }
    return 1;
}
 
Since I am using "assigns \nothing;" I expect the term \old() in comparison to be obsolete.
 
But as I recall, assigns \nothing allows temorary modification, as long as the content of the elements mentioned in
the parameter list of the function is restored before termination.
 
So I modified the algorithm, to alter the memory and restore it, allowing the algorithm to return allways
"true":
 
 
/*@
    requires 0 <= length;
    requires \valid_range (a, 0, length-1);
    requires \valid_range (b, 0, length-1);
 
    assigns \nothing;
    
    behavior equal:
        ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> a[i] == b[i]);
    behavior not_equal:
        ensures \result == 0 <==> (\exists integer i; 0 <= i < length && a[i] != b[i]);
*/
int equal_array (int* a, int length, int* b )
{
 
    int save_array_a[length];
    int save_array_b[length];
 
    /*@
        loop invariant 0 <= i <= length;
        loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k] == 0;
        loop invariant \forall integer k; 0 <= k < i ==> a[k] == save_array_a[k];
        loop invariant \forall integer k; 0 <= k < i ==> b[k] == save_array_b[k];
    */
    for(int i = 0; i < length; i++)
    {
        save_array_a[i] = a[i];
        save_array_b[i] = b[i];
        a[i] = 0;
        b[i] = 0;
    }
 
    int index_a = 0;
    int index_b = 0;
    /*@
        loop invariant 0 <= index_a <= length;
        loop invariant 0 <= index_b <= length;
        loop invariant index_a == index_b;
        loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == b[k];
    */
    while ( index_a != length )
    {
        if (a[index_a] != b[index_b])
            return 0;
        ++index_a;
        ++index_b;
   }
 
 
    /*@
        loop invariant 0 <= i <= length;
        loop invariant \forall integer k; 0 <= k < i ==> a[k] == save_array_a[k];
        loop invariant \forall integer k; 0 <= k < i ==> b[k] == save_array_b[k];
    */
    for(int i = 0; i < length; i++)
    {
        a[i] = save_array_a[i];
        b[i] = save_array_b[i];
    }
    return 1;
}
 
 
My problem:
 
I cannot invoke the Jessie gui, it stops with the message:
 
equal_array.c:6: Warning: Variable-sized local variable save_array_a
equal_array.c:7: Warning: Variable-sized local variable save_array_b
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
No code for function __builtin_alloca, default assigns generated
Producing Jessie files in subdir equal_array.jessie
File equal_array.jessie/equal_array.jc written.
File equal_array.jessie/equal_array.cloc written.
Calling Jessie tool in subdir equal_array.jessie
Generating Why function equal_array
File "jc/jc_interp.ml", line 861, characters 11-11:
Uncaught exception: File "jc/jc_interp.ml", line 861, characters 11-17: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs e
qual_array.cloc equal_array.jc
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000195)
signoles (manager)
2009-06-17 13:28

No more assertion raised: the jessie gui is opened.

- Issue History
Date Modified Username Field Change
2009-04-07 14:07 virgile New Issue
2009-04-07 15:42 signoles Status new => acknowledged
2009-04-10 10:06 signoles Status acknowledged => assigned
2009-04-10 10:06 signoles Assigned To => cmarche
2009-06-17 13:28 signoles Note Added: 0000195
2009-06-17 13:28 signoles Status assigned => resolved
2009-06-17 13:28 signoles Fixed in Version => Frama-C Beryllium beta-1
2009-06-17 13:28 signoles Resolution open => fixed
2009-06-23 18:02 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker