/* 
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
  KaRaMeL invocation: krml -skip-compilation -warn-error +9 out.krml
  F* version: 58c915a8
  KaRaMeL version: 22425a93
 */

#include "Tuto.h"

uint32_t Tuto_x = 0U;

uint32_t Tuto_x_real = 0U;

uint32_t Tuto_x_shifted;

void Tuto_f(void)
{
  uint32_t *r = KRML_HOST_CALLOC(16U, sizeof (uint32_t));
  r[0U] = 1U;
}

void Tuto_incr(uint32_t *r, uint32_t *other)
{
  KRML_MAYBE_UNUSED_VAR(other);
  uint32_t r_v = r[0U];
  r[0U] = r_v + 1U;
}

void Tuto_call_incr(void)
{
  uint32_t r = 0U;
  uint32_t other[8U] = { 0U };
  Tuto_incr(&r, other);
}

FStar_Pervasives_Native_option__uint32_t Tuto_sum_low(uint32_t *b, uint32_t len)
{
  FStar_Pervasives_Native_option__uint32_t r = { .tag = FStar_Pervasives_Native_Some, .v = 0U };
  for (uint32_t i = 0U; i < len; i++)
  {
    FStar_Pervasives_Native_option__uint32_t r_v = r;
    if (!(r_v.tag == FStar_Pervasives_Native_None))
      if (r_v.tag == FStar_Pervasives_Native_Some)
      {
        uint32_t r_v1 = r_v.v;
        uint32_t b_i = b[i];
        if (i == 0U)
          r =
            (
              (FStar_Pervasives_Native_option__uint32_t){
                .tag = FStar_Pervasives_Native_Some,
                .v = b_i
              }
            );
        else if (r_v1 > 0xffffffffU - b_i)
          r = ((FStar_Pervasives_Native_option__uint32_t){ .tag = FStar_Pervasives_Native_None });
        else
          r =
            (
              (FStar_Pervasives_Native_option__uint32_t){
                .tag = FStar_Pervasives_Native_Some,
                .v = r_v1 + b_i
              }
            );
      }
      else
      {
        KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
          __FILE__,
          __LINE__,
          "unreachable (pattern matches are exhaustive in F*)");
        KRML_HOST_EXIT(255U);
      }
  }
  return r;
}

bool Tuto_sum_low2(uint32_t *uu___, uint32_t *uu___1, uint32_t uu___2)
{
  KRML_MAYBE_UNUSED_VAR(uu___);
  KRML_MAYBE_UNUSED_VAR(uu___1);
  KRML_MAYBE_UNUSED_VAR(uu___2);
  KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "");
  KRML_HOST_EXIT(255U);
}