Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2525

Lithium fool the tool

ID0000029: This issue was created automatically from Mantis Issue 29. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000029 Frama-C Plug-in > jessie public 2009-04-07 2009-06-23
Reporter virgile Assigned To cmarche Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Lithium-20081201 Target Version - Fixed in Version Frama-C Beryllium-20090601-beta1

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking