Michele Alberti authored 4 years ago and David Bühler committed 3 years ago

[Eva] Rework assign support so that control and data dependency taint analysis are performed as not alternatives to each other.

Michele Alberti authored 4 years ago and David Bühler committed 3 years ago

[Eva] Revise assign so that if the left-value appears in statement annotation, then it will always be considered tainted.

Without this commit, an assignment 'x = 3' with annotation '//@ taint x;' would had not resulted in 'x' as tainted because '3' is a literal, hence not tainted.

Michele Alberti authored 4 years ago and David Bühler committed 3 years ago

[Eva] Rework finalize_call so that resulting control statement is defined as the one in the pre abstract state.

Michele Alberti authored 4 years ago and David Bühler committed 3 years ago

[Eva] In assume, update state's control statement also when the current one is to be tainted and outside the scope of the former.

(blind make headers from specifications)

- Fix Value/Value#5
- Fix Value/Value#14

Some case studies (e.g. dyad) use some ugly casts from fd_set_t which lead
to the analysis stopping too early.
Changing the representation of fd_set_t should also help it better conform to
the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).