fix: prevent ub, always havoc after malloc

[priyasiddharth]

1. Document differences between seahorn, fuzz, klee and smack -- in some cases, malloc fails, in others it does not
2. Rename malloc to malloc_havoc to clarify what is expected to happen

[agurfinkel]

LGTM

[LinerSu]

FUZZ got failing. @danblitzhou is that necessary to enable fuzzing test under Seahorn CI?

verify-c-common/docker/verify-c-common.Dockerfile

Line 33 in cf2f76d

RUN mkdir build && cd build && cmake -DSEA_LINK=llvm-link-10 -DCMAKE_C_COMPILER=clang-10 -DCMAKE_CXX_COMPILER=clang++-10 -DSEAHORN_ROOT=/home/usea/seahorn -DSEA_ENABLE_FUZZ=ON -Daws-c-common_DIR=$(pwd)/../aws-c-common/build/run/lib/aws-c-common/cmake/ ../ -GNinja && cmake --build .

[danblitzhou]

FUZZ got failing. @danblitzhou is that necessary to enable fuzzing test under Seahorn CI?

verify-c-common/docker/verify-c-common.Dockerfile

Line 33 in cf2f76d

RUN mkdir build && cd build && cmake -DSEA_LINK=llvm-link-10 -DCMAKE_C_COMPILER=clang-10 -DCMAKE_CXX_COMPILER=clang++-10 -DSEAHORN_ROOT=/home/usea/seahorn -DSEA_ENABLE_FUZZ=ON -Daws-c-common_DIR=$(pwd)/../aws-c-common/build/run/lib/aws-c-common/cmake/ ../ -GNinja && cmake --build .

this seems like a mistake, we have a separate fuzzing dockerfile; will turn this off in a PR

[codecov]

Codecov Report

Merging #114 (6777f6f) into master (431bbe7) will increase coverage by 1.37%.
The diff coverage is 98.07%.

@@            Coverage Diff             @@
##           master     #114      +/-   ##
==========================================
+ Coverage   93.74%   95.12%   +1.37%     
==========================================
  Files         159      159              
  Lines        4907     4919      +12     
==========================================
+ Hits         4600     4679      +79     
+ Misses        307      240      -67     

Impacted Files	Coverage Δ
seahorn/include/proof_allocators.h	100.00% <ø> (ø)
..._dynamic/aws_priority_queue_init_dynamic_harness.c	100.00% <ø> (ø)
...it_static/aws_priority_queue_init_static_harness.c	100.00% <ø> (ø)
seahorn/lib/fuzz_array_list_helper.c	74.19% <50.00%> (ø)
...n/jobs/array_eq_c_str/aws_array_eq_c_str_harness.c	94.87% <100.00%> (ø)
...jobs/array_list_back/aws_array_list_back_harness.c	100.00% <100.00%> (ø)
...bs/array_list_front/aws_array_list_front_harness.c	100.00% <100.00%> (ø)
.../array_list_get_at/aws_array_list_get_at_harness.c	100.00% <100.00%> (ø)
...ist_get_at_ptr/aws_array_list_get_at_ptr_harness.c	100.00% <100.00%> (ø)
...t_init_static/aws_array_list_init_static_harness.c	100.00% <100.00%> (ø)
... and 26 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 431bbe7...6777f6f. Read the comment docs.

[LinerSu]

Are we assuming fuzz always returns a true value after invoking nd_bool?

[priyasiddharth]

No, we get the next sizeof(bool) data. If it is zero then we return false.

[priyasiddharth]

nospec test is failing on azure. Will accept PR and debug in master