mikhailramalho

#include <math.h>
#include <assert.h>

float nondet();

int main(void)
{
  float from = 2.155872e+9f;
  union {
    float a;

mikhailramalho

#include <math.h>
#include <assert.h>

float nondet();

int main(void)
{
  float from = nondet();
  __ESBMC_assume(from > 0.0f);
  __ESBMC_assume(!isinf(from));

mikhailramalho

#include <math.h>
#include <assert.h>

float my_nextafterf( float from, float to )
{
  union {
    float a;
    int b;
  } from_union = { .a = from };

mikhailramalho

#include <assert.h>
#include <math.h>
#include <fenv.h>

int main (void) {
  float f;
  float g;

  __ESBMC_assume(!isnan(f));
  __ESBMC_assume(!isnan(g));

mikhailramalho

typedef struct {
    _Bool is_float;
    union {
       float f;
       double s;
    };
} mychoice_t;

double as_float(mychoice_t* ch) 
{ 

mikhailramalho

unsigned int calc_size(unsigned int size)
{
  return size*2;
}

void VLA_size(unsigned int size)
{
  int arr[calc_size(size)];
  arr[calc_size(size)-1] = 1;

mikhailramalho

#include <assert.h>

unsigned int my_strlen(const char* s)
{
  const char *eos = s;
  while (*eos++);
  return (int) (eos - s - 1);
}

int main() 

mikhailramalho

struct X { int a; };
 
typedef const _Bool inteiro;
 
const unsigned int d = 10;
const unsigned int c = d;
const unsigned int f = d;

int fun4(int x, int y) { return x/f; }