MemSafety Low-Hanging Fruit

[michael-schwarz]

For some reason, we fail to show the InvalidDeref-MemSafety part for this trivial program.

#include <pthread.h>
#include <goblint.h>

struct twoIntsStruct {
   int intOne ;
   int intTwo ;
};


int main(int argc, char **argv)
{
  struct twoIntsStruct *data;
  data = (struct twoIntsStruct *)calloc(100UL,8UL);

  data->intOne = 0;
  data->intTwo = 0;
}

[Warning][Unknown] Size of lval dereference expression data is top. Out-of-bounds memory access may occur (1.c:16:3-16:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer data is top. Memory out-of-bounds access might occur due to pointer arithmetic (1.c:16:3-16:19)
[Warning][Unknown] Size of lval dereference expression data is top. Out-of-bounds memory access may occur (1.c:17:3-17:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer data is top. Memory out-of-bounds access might occur due to pointer arithmetic (1.c:17:3-17:19)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (1.c:18:1-18:1)

[michael-schwarz]

This subfruit hangs so low it touches the ground even:

// PARAM: --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"
#include <pthread.h>
#include <goblint.h>

int main(int argc, char **argv)
{
  int* dPtr = calloc(100UL,8UL);
  *dPtr = 8;
}

[jerhard]

This subfruit hangs so low it touches the ground even:

What result do you get, and on which branch/commit?

When I run this test, I get

SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Debug][Analyzer] Base EvalInt tmp query answering bot instead of {&(alloc@sid:1@tid:[main](#top))[def_exc:0]} (tests/regression/76-memleak/21-mem-safety.c:7:6-7:32)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 4
  dead: 0
  total lines: 4
SV-COMP result: true
Writing xml to temp. file: /tmp/ocaml2c9f0ctmp
Time needed: 604 ms
See result/index.xml

The [Debug][Analyzer] Base EvalInt tmp query answering bot instead of {&(alloc@sid:1@tid:[main](#top))[def_exc:0]} (tests/regression/76-memleak/21-mem-safety.c:7:6-7:32) disaapears, if I add #include <stdlib.h> to the C file.

Edit: Probably has to do with the specification. Which one did you test?

[michael-schwarz]

MemSafety was the one I tested. Here, the malloc works and the calloc fails.

//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins --set ana.activated[+] memOutOfBounds --enable ana.int.interval
#include <pthread.h>
#include <goblint.h>

int main(int argc, char **argv)
{
  int* ptrCalloc = calloc(100UL,8UL);
  *ptrCalloc = 8; //NOWARN

  int* ptrMalloc = malloc(800UL);
  *ptrMalloc = 8; //NOWARN
}