Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

Code Block
bgColor#ccccff
langc
unsigned int ui_a;
unsigned int ui_b;
unsigned int udiff;

void func(void) {
  /* Initialize ui_a and ui_b */

  if (ui_a < ui_b){
    /* Handle error condition */
  } else {
    udiff = ui_a - ui_b;
  }

  /* ... */
}

...

This compliant solution performs a postcondition test to ensure that the result of the unsigned addition operation to i is not less than the operand ui_a:

 

Code Block
bgColor#ccccff
langc
#include <stdatomic.h>
 
atomic_int i;
int ui_a;

void func(void) {
  /* Initialize ui_a, i*/
 
  atomic_fetch_add(&i, ui_a);
  if (atomic_load(&i) < ui_a) {
    /* Handle error condition */
  }
  /* ... */
}

Exceptions

...