malloc.res.oracle

[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
[instantiate] tests/stdlib/malloc.c:21: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
   int x ;
   int y ;
};
struct Flex {
   int x ;
   char c ;
   int f[] ;
};
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,size);
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
struct Flex *malloc_st_Flex(size_t size)
{
  struct Flex *__retres;
  __retres = (struct Flex *)malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 40;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,size);
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
int (*malloc_arr10_int(size_t size))[10]
{
  int (*__retres)[10];
  __retres = (int (*)[10])malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 1;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,size);
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
char *malloc_char(size_t size)
{
  char *__retres;
  __retres = (char *)malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 8;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,size);
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
struct X *malloc_st_X(size_t size)
{
  struct X *__retres;
  __retres = (struct X *)malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 4;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,size);
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
float *malloc_float(size_t size)
{
  float *__retres;
  __retres = (float *)malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 4;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,size);
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
int *malloc_int(size_t size)
{
  int *__retres;
  __retres = (int *)malloc(size);
  return __retres;
}

int main(void)
{
  int __retres;
  int *pi = malloc_int(sizeof(int) * (unsigned int)10);
  float *pf = malloc_float(sizeof(float) * (unsigned int)10);
  struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
  char *pc = malloc_char((unsigned int)10);
  int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
  struct Flex *f =
    malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
  void *v = malloc(sizeof(char) * (unsigned int)10);
  __retres = 0;
  return __retres;
}


[kernel] Parsing tests/stdlib/result/malloc.c (with preprocessing)
[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
[kernel] tests/stdlib/malloc.c:14: Warning: 
  def'n of func main at tests/stdlib/malloc.c:14 (sum 6403) conflicts with the one at tests/stdlib/result/malloc.c:198 (sum 8177); keeping the one at tests/stdlib/result/malloc.c:198.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
   int x ;
   int y ;
};
struct Flex {
   int x ;
   char c ;
   int f[] ;
};
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
struct Flex *malloc_st_Flex(size_t size)
{
  struct Flex *__retres;
  __retres = (struct Flex *)malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 40;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
int (*malloc_arr10_int(size_t size))[10]
{
  int (*__retres)[10];
  __retres = (int (*)[10])malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 1;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
char *malloc_char(size_t size)
{
  char *__retres;
  __retres = (char *)malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 8;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
struct X *malloc_st_X(size_t size)
{
  struct X *__retres;
  __retres = (struct X *)malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 4;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
float *malloc_float(size_t size)
{
  float *__retres;
  __retres = (float *)malloc(size);
  return __retres;
}

/*@ requires correct_size: 0 ≡ size % 4;
    assigns \result, __fc_heap_status;
    assigns \result \from __fc_heap_status, size;
    assigns __fc_heap_status \from __fc_heap_status, size;
    allocates \result;
    
    behavior allocation:
      assumes allocable: is_allocable(size);
      ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
      assigns \result, __fc_heap_status;
      assigns \result \from __fc_heap_status, size;
      assigns __fc_heap_status \from __fc_heap_status, size;
      allocates \result;
    
    behavior no_allocation:
      assumes allocable: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
int *malloc_int(size_t size)
{
  int *__retres;
  __retres = (int *)malloc(size);
  return __retres;
}

int main(void)
{
  int __retres;
  int *pi = malloc_int(sizeof(int) * (unsigned int)10);
  float *pf = malloc_float(sizeof(float) * (unsigned int)10);
  struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
  char *pc = malloc_char((unsigned int)10);
  int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
  struct Flex *f =
    malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
  void *v = malloc(sizeof(char) * (unsigned int)10);
  __retres = 0;
  return __retres;
}