Calling add  #107

Activity

1. dc-mak commented on Dec 27, 2024

   

   dc-mak

   on Dec 27, 2024

   Collaborator

   More actions

   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
2. r-ross commented on Jan 3, 2025

   

   r-ross

   on Jan 3, 2025

   More actions

   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.
3. dc-mak commented on Jan 4, 2025

   

   dc-mak

   on Jan 4, 2025

   Collaborator

   More actions

   Please submit a PR if it's urgent.
4. dc-mak

   closed this as completedon Jan 4, 2025
5. dc-mak

   reopened this on Jan 4, 2025
6. lwli11 commented on Jan 6, 2025

   

   lwli11

   on Jan 6, 2025

   Author

   More actions

   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);
           }
   }