source: CIVL/mods/dev.civl.com/examples/contracts/result.c@ cb4d4f4

#include<assert.h>

int gimmeOne() 
  $ensures {$result == 1} {
  return 1;
}

int main() {
  int x = gimmeOne();

  assert(x == 1);
}