exec.res.oracle

[variadic] FRAMAC_SHARE/libc/unistd.h:795: 
  Declaration of variadic function execl.
[variadic] FRAMAC_SHARE/libc/unistd.h:800: 
  Declaration of variadic function execle.
[variadic] FRAMAC_SHARE/libc/unistd.h:805: 
  Declaration of variadic function execlp.
[variadic] tests/known/exec.c:9: Translating call to execle to a call to execve.
[variadic] tests/known/exec.c:11: Warning: 
  Too many arguments: expected 5, given 6. Superfluous arguments will be removed.
[variadic] tests/known/exec.c:11: Translating call to execl to a call to execv.
[variadic] tests/known/exec.c:12: Warning: 
  Too many arguments: expected 4, given 5. Superfluous arguments will be removed.
[variadic] tests/known/exec.c:12: 
  Translating call to execlp to a call to execvp.
[variadic] tests/known/exec.c:13: Warning: 
  Too many arguments: expected 4, given 6. Superfluous arguments will be removed.
[variadic] tests/known/exec.c:13: 
  Translating call to execle to a call to execve.
[variadic] tests/known/exec.c:15: Warning: 
  Failed to find a sentinel (NULL pointer) in the argument list.
[variadic] tests/known/exec.c:15: 
  Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function execve
[eva] using specification for function execv
[eva] using specification for function execvp
[eva] using specification for function execlp
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  env[0] ∈ {{ "VAR=42" }}
     [1] ∈ {0}
  sentinel ∈ {0}
  __retres ∈ {0}
/* Generated by Frama-C */
#include "sys/time.h"
#include "unistd.h"
int main(void)
{
  int __retres;
  char *env[2] = {(char *)"VAR=42", (char *)0};
  char *sentinel = (char *)0;
  {
    char * const argv[4] =
      {(char *)"sh", (char *)"-c", (char *)"echo $VAR", (char *)0};
    execve("/bin/sh",argv,(char * const *)(env));
  }
  {
    char * const argv_5[4] =
      {(char *)"ls", (char *)"-l", (char *)"--color", (char *)0};
    int tmp = 42;
    execv("ls",argv_5);
  }
  {
    char * const argv_8[3] = {(char *)"ls", (char *)"-all", (char *)0};
    void *tmp_10 = (void *)0;
    execvp("ls",argv_8);
  }
  {
    char * const argv_12[2] = {(char *)"ls", (char *)0};
    int tmp_14 = 42;
    void *tmp_16 = (void *)0;
    execve("ls",argv_12,(char * const *)(env));
  }
  {
    char const *__va_arg0 = "--reverse";
    char *__va_arg1 = sentinel;
    void *__va_args[2] = {& __va_arg0, & __va_arg1};
    execlp("ls","ls",(void * const *)(__va_args));
  }
  __retres = 0;
  return __retres;
}