Calling add

[lwli11]

As a follow-on to writing the spec for add_0.c, it would be nice to have a tutorial for how a function can call add(x, y). We've run into a similar issue, and I'm not sure how to write the code to fulfill add(x,y)'s require clause. It's like:

int anotherfunc(...){
...
//calculate x
//calculate y
if (???){ //Not sure what to put here.
add(x,y);
}
}

Thanks!

[dc-mak]

Remember that specifications are always defined/meaningful.
Both signed and unsigned integer addition in the specs are allowed to overflow, so we can take advantage of that.
This is what I came up with...

int add(int x, int y)
/*@ requires (x >= 0i32 || y >= 0i32) implies x <= x + y && y <= x + y;
             x <  0i32 && y <  0i32 implies x + y <= x && x + y <= y;
    ensures return == x + y;
@*/
{
    return x + y;
}

You could always try to just copy secure coding standards into specs, but I think that would be ugly
https://wiki.sei.cmu.edu/confluence/display/c/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow

[r-ross]

Isn't that spec wrong, e.g, when x is 1 and y is -3? The link has a proper check in the "Compliant Solution" subsection of "Addition". Consider providing an example spec based on that and mentioning the link in the tutorial to help others.

[dc-mak]

Please submit a PR if it's urgent.

[lwli11]

In the original question, I was actually asking what to put in the if (...) of the function "another_func" which is calling add. Copying from the coding standards guide, the IF statement is still not sufficient though:

Here's the self-contained code of a representative example of what we're trying to do.

#include <limits.h>
typedef struct mysteryStruct
{
        int val;
} mysteryStruct_t;
mysteryStruct_t add(mysteryStruct_t x, mysteryStruct_t y)
/*@
        requires let sumx = (i64) x.val + (i64) y.val;
        sumx > (i64) MINi32(); sumx<(i64) MAXi32();
        ensures true;
@*/
{
        y.val = x.val + y.val;
        return y;
}

extern int createInt();
/*@
        spec createInt();
        requires true;
        ensures return>MINi32() && return < MAXi32();
@*/


void another_func(){
        mysteryStruct_t x = {0};
        mysteryStruct_t y = {0};
        x.val = createInt();
        y.val = createInt();
       //TODO: This IF isn't sufficient
        if (!((y.val > 0) && (x.val > (INT_MAX - y.val))) &&
        !((y.val < 0) && (x.val < (INT_MIN - y.val)))){
                add(x, y);
        }
}