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.

Feature/from vanadium

See merge request frama-c/frama-c!3200

Feature/andre/libc some coreutils

See merge request frama-c/frama-c!3186

[kernel] Do not mark a specification as generated if the generation fails.

See merge request frama-c/frama-c!3202

Fixes a crash when re-running an analysis.

[kernel] Rejects bitfields with negative width. Avoids later crash in analyses.

See merge request frama-c/frama-c!3201

[Eva] User manual: documents the analysis of recursive calls

See merge request frama-c/frama-c!3193