fix all warnings, add most missing algos, revamp algorithms.h #31
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
rurban
force-pushed
the
new
branch
7 times, most recently
from
3de7222 to
c3dcb9b
Compare
rurban
changed the title
rurban
changed the title
|
Hi, I'm only a contributor to this repo, so won't be reviewing this PR. However, this is a huge amount of change for a single PR. You should consider splitting up your changes into smaller and more focused PRs. This will be easier to review and approve. |
|
Also, hasn't been much activity on this repo for a while. Not sure to what extent it is still being maintained. Don't want you to waste your great effort here! |
esp. new source/*.c strcpy
the algo should be realistic, not synthetic. we need to optionally store the indices. Add a DEBUG mode to print the found indices for control.
only detected by clang -Wextra
but no OUTPUT support yet
fixes the random sanitizer errors
missed that. fixes more random sanitizer errors.
tsa still failing randonly with binary texts. gs asserts. now passing: ms, nsn, dfdm, sbndmq6, sbndmq8, ufndmq2, ufndmq4, ufndmq6, ufndmq8, sabp, dbww, dbww2, ksa, kbndm, bsdm
run each size explicitly, not via nondet_int < MAX_M
extend cbmc to check MIN_M, MAX_M split cbmc and fuzz headers from main.h
dump t[n]
to repro fuzz crashes
else we get T buffer overflows
dump t[n]
better than printable. usage: make CFLAGS="-g -DNOSHM" SANITIZE=1 gcc -O0 -DNOSHM -march=native -mtune=native -Wall -Wfatal-errors -g -Wextra -fsanitize=address,undefined -DBINDIR=\"bin/asan\" source/test.c -std=gnu99 -o test-asan -lm ./test-asan bxs4 --files fuzz/bxs4/default/crashes/id:000000,sig:11,src:000017,time:25,execs:1567,op:havoc,rep:3 fuzz/bxs4/default/data.t ~
because we test now $'\x00' args
fix for older cbmc (no __CPROVER_loop_invariant)
and fixed tndma
still verified successful, even if its broken. also fix a MAX_M overflow in the verifier.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
and add a proper Makefile.
algorithms.h is now static