[wp] type logic function _calls_ with C type

Closes #1332

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

Remove unnecessary parameters from doinit

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

Merge branch 'fix/martin/kernel/1366-error-messages-when-a-function-is-redeclared-with-incompatible-types' into 'master'

Resolve "Error messages when a function is redeclared with incompatible types"

Closes #1366

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

Merge branch 'fix/martin/kernel/1293-misleading-api-function-annotations-iter_behaviors' into 'master'

Resolve "Misleading API function Annotations.iter_behaviors"

Closes #1293

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

Fix/libc/pthread t portability

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

Add an option in test script to launch Dune in watch mode

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

[ivette] using Vite packager

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

[Eva] Reduction on ACSL valid_string and valid_read_string predicates

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

[gui] Fix menu item labels alignment

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

David Bühler authored 1 year ago and Andre Maroneze committed 11 months ago

This test contained sure undefined behaviors that would lead to bottom when
reducing values on ACSL predicates valid_string and valid_read_string.

David Bühler authored 1 year ago and Andre Maroneze committed 11 months ago

During the interpretation of a function call, the possible values of formal
parameters can be reduced — especially by the evaluation of the function
preconditions.
At the end of a function call, Eva backward propagates these reductions to the
concrete arguments of the call.

This commit also does this backward-propagation when a builtin is used to
interpret the call.

Also removes unused [builtin] field from call results (it was only used to
avoid the backward propagation of argument reductions when a builtin was used).

Rework CurrentLoc for better consistency

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