weird behaviour of assume with function arguments ?

5 views
Skip to first unread message

Ramon Bejar Torres

unread,
May 26, 2021, 11:23:01 AM5/26/21
to CProver Support
Hi All,
I have found while working with some stundents a weird behavior with assume. Consider this file  (asc2.c):

#define N 20

int ascending(   int a[N] ) {
  int d, k;
  // int a[N];  (if a[N] is a local variable, then the example works OK)
  
   __CPROVER_assume( (a[0] == 0)  ); 
   d = a[0];
   k= 2;
   k = 3;
   d = a[0];
    __CPROVER_assert( d == 0 , "a[0] is 0" );
  
 }

when verified with cbmc 5-11 over Ubuntu , with flags:
   cbmc --trace --function ascending asc2.c

I get this counterexample (from line 8):

State 28 file asc2.c function ascending line 8 thread 0
----------------------------------------------------
  d=0 (00000000 00000000 00000000 00000000)

State 29 file asc2.c function ascending line 9 thread 0
----------------------------------------------------
  k=2 (00000000 00000000 00000000 00000010)

State 30 file asc2.c function ascending line 10 thread 0
----------------------------------------------------
  k=3 (00000000 00000000 00000000 00000011)

State 31 file asc2.c function ascending line 11 thread 0
----------------------------------------------------
  d=1 (00000000 00000000 00000000 00000001)

Violated property:
  file asc2.c function ascending line 12 thread 0
  a[0] is 0
  d == 0

So, it seems that a[0] changed from 0 to 1 (but the program did not change a[1]).
But if the array a[N] is created as a local variable, and not a parameter of the function, then the property checks OK.
Is this beacuse are we assuming that other "thread" can be modifying the array a[] ?  But If do not have any other threads in this simple program.

Regards,
Ramon Béjar
University of Lleida
 

Ramon Bejar Torres

unread,
May 26, 2021, 11:35:47 AM5/26/21
to CProver Support
Sorry, where I say:
  ->  So, it seems that a[0] changed from 0 to 1 (but the program did not change a[1])
I wanted to say:
So, it seems that a[0] changed from 0 to 1 (but the program did not change a[0])

Martin Nyx Brain

unread,
May 26, 2021, 1:36:48 PM5/26/21
to cprover...@googlegroups.com
On Wed, 2021-05-26 at 08:23 -0700, Ramon Bejar Torres wrote:
> Hi All,
> I have found while working with some stundents a weird behavior with
> assume. Consider this file (asc2.c):
>
> #define N 20
>
> int ascending( int a[N] ) {
> int d, k;
> // int a[N]; (if a[N] is a local variable, then the example works
> OK)
>
> __CPROVER_assume( (a[0] == 0) );
> d = a[0];
> k= 2;
> k = 3;
> d = a[0];
> __CPROVER_assert( d == 0 , "a[0] is 0" );
>
> }

<snip>

> So, it seems that a[0] changed from 0 to 1 (but the program did not
> change
> a[1]).
> But if the array a[N] is created as a local variable, and not a
> parameter
> of the function, then the property checks OK.
> Is this beacuse are we assuming that other "thread" can be modifying
> the
> array a[] ? But If do not have any other threads in this simple
> program.

This is not intended behaviour; it shouldn't change. There are a
number of things that might cause this:

1. Generally, I would recommend using a newer CBMC version

https://github.com/diffblue/cbmc/releases

a lot has changed since 5.11.


2. Arrays as arguments, particularly to the main function lands you in
the world of "it's not 100% clear what the correct behaviour should
be". If CBMC is called with --function f00 where f00 takes a pointer
it is hard to work out what it should point to, should it be a valid
region, if so, how large, etc. It is better to structure the code as:

#define N 20

int ascending(int *array) {
// ...
}

int main (int argc, char **argv) {
// Build the environment here
int array[N];

ascending(array);

return 0;
}


3. There is a bug in the native back-end which affects equality between
arrays of non-constant size. It is only triggered in unusual use cases
and I haven't found an easy test case. It is possible that your code
is one. One check is whether this fails when run with an SMT solver.

HTH

Cheers,
- Martin


Reply all
Reply to author
Forward
0 new messages