snprintf.res.oracle

[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
  Declaration of variadic function fprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
  Declaration of variadic function fscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
  Declaration of variadic function printf.
[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
  Declaration of variadic function scanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
  Declaration of variadic function snprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
  Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
  Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
  Declaration of variadic function dprintf.
[variadic] tests/known/snprintf.c:12: 
  Translating call to snprintf to a call to the specialized version snprintf_va_1.
[variadic] tests/known/snprintf.c:15: 
  Translating call to snprintf to a call to the specialized version snprintf_va_2.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] FRAMAC_SHARE/libc/string.h:118: 
  cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] using specification for function snprintf_va_1
[eva] tests/known/snprintf.c:12: 
  Cannot evaluate range bound format_length(format) - 1
  (unsupported ACSL construct: logic function format_length). Approximating
[eva:alarm] tests/known/snprintf.c:12: Warning: 
  function snprintf_va_1: precondition \valid(s + (0 .. n - 1)) ∨
                                       \valid(s +
                                              (0 .. format_length(format) - 1)) got status unknown.
[eva:alarm] tests/known/snprintf.c:13: Warning: 
  assertion got status invalid (stopping propagation).
[eva] using specification for function snprintf_va_2
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  data[0..98] ∈ {65}
      [99] ∈ {0}
  dest[0..49] ∈ [--..--]
  __retres ∈ {0}
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
#include "string.h"
#include "strings.h"
int volatile nondet;
/*@ requires
      \valid(s + (0 .. n - 1)) ∨
      \valid(s + (0 .. format_length(format) - 1));
    requires valid_read_string(format);
    requires valid_read_string(param0);
    assigns \result, *(s + (0 ..));
    assigns \result
      \from (indirect: n), (indirect: *(format + (0 ..))),
            (indirect: *(param0 + (0 ..)));
    assigns *(s + (0 ..))
      \from (indirect: n), (indirect: *(format + (0 ..))), *(param0 + (0 ..));
 */
int snprintf_va_1(char * __restrict s, size_t n,
                  char const * __restrict format, char *param0);

/*@ requires
      \valid(s + (0 .. n - 1)) ∨
      \valid(s + (0 .. format_length(format) - 1));
    requires valid_read_string(format);
    requires valid_read_string(param0);
    assigns \result, *(s + (0 ..));
    assigns \result
      \from (indirect: n), (indirect: *(format + (0 ..))),
            (indirect: *(param0 + (0 ..)));
    assigns *(s + (0 ..))
      \from (indirect: n), (indirect: *(format + (0 ..))), *(param0 + (0 ..));
 */
int snprintf_va_2(char * __restrict s, size_t n,
                  char const * __restrict format, char *param0);

int main(void)
{
  int __retres;
  char data[100];
  size_t tmp_0;
  memset((void *)(data),'A',(unsigned int)99);
  data[99] = (char)0;
  char dest[50] = {(char)'\000'};
  if (nondet) {
    size_t tmp;
    tmp = strlen((char const *)(data));
    snprintf_va_1(dest,tmp,"%s",data);
    /*@ assert \false; */ ;
  }
  tmp_0 = strlen((char const *)(data));
  snprintf_va_2(dest,tmp_0 / (size_t)2,"%s",data);
  __retres = 0;
  return __retres;
}