diff --git a/regression/goto-analyzer-taint-ansi-c/Makefile b/regression/goto-analyzer-taint-ansi-c/Makefile new file mode 100644 index 00000000000..462e051669c --- /dev/null +++ b/regression/goto-analyzer-taint-ansi-c/Makefile @@ -0,0 +1,19 @@ +default: tests.log + +test: + @../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer + +tests.log: ../test.pl + @../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.java" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.c b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.c new file mode 100644 index 00000000000..806b14fa2b4 --- /dev/null +++ b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.c @@ -0,0 +1,15 @@ +#include + +void my_f(void *) { } +void my_h(void *) { } + +void my_function() +{ + void *o1; + my_f(o1); // T1 source + + void *o2; + memcpy(o2, o1, 100); + + my_h(o2); // T1 sink +} diff --git a/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.o b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.o new file mode 100644 index 00000000000..566d8da99a7 Binary files /dev/null and b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.o differ diff --git a/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/taint.json b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/taint.json new file mode 100644 index 00000000000..44a841f0cc4 --- /dev/null +++ b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/taint.json @@ -0,0 +1,4 @@ +[ +{ "id": "my_f", "kind": "source", "where": "parameter1", "taint": "T1", "function": "my_f" }, +{ "id": "my_h", "kind": "sink", "where": "parameter1", "taint": "T1", "function": "my_h", "message": "There is a T1 flow" } +] diff --git a/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/test.desc b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/test.desc new file mode 100644 index 00000000000..af2d62eb456 --- /dev/null +++ b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/test.desc @@ -0,0 +1,7 @@ +CORE +main.o +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file main.c line 12( function .*)?: There is a T1 flow \(taint rule my_h\)$ +-- diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index a0d835dd865..906365b97a8 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -380,6 +380,19 @@ void custom_bitvector_domaint::transform( } } } + else if(identifier=="memcpy" || + identifier=="memmove") + { + if(code_function_call.arguments().size()==3) + { + // we copy all tracked bits from op1 to op0 + // we do not consider any bits attached to the size op2 + dereference_exprt lhs_deref(code_function_call.arguments()[0]); + dereference_exprt rhs_deref(code_function_call.arguments()[1]); + + assign_struct_rec(from, lhs_deref, rhs_deref, cba, ns); + } + } else { goto_programt::const_targett next=from;