Skip to content
Snippets Groups Projects
Commit 7ce18d3c authored by Boris Yakobowski's avatar Boris Yakobowski Committed by David Bühler
Browse files

[Tests] do not use Frama_C_foo directly

Instead, include the proper libc headers, with the specifications.
Otherwise, in the next commits(s), we won't have preconditions to evaluate, and the tests
will be come unsound

Changes:

- share/libc/stdlib.c: previous version of calloc in stdlib. used Frama_C_memset, which is idiotic since
  - for non-free we now *have* a builtin for calloc
  - stdlib.c is meant for people with non-free builtins

- same thing for tests/libs/string_c.c: the builtin was used

- nonfree/imprecise.c:
  sizeof(v3), where v3 is an abstract struct, is evaluated slightly less precisely now.
  We don't care as long as it does not crash.

- nonfree/strchr.c:
  the test is buggy, the behavior was undefined
parent f7bea823
No related branches found
No related tags found
No related merge requests found
Showing
with 478 additions and 316 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment