[Logic] accepts integer/real as C fields

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

[configure] Accept packages with symbol '.' in the name.

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

[Eva] Fixes request getDeadCode for functions that have not been analyzed.

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

[Eva] API: exports analysis computation state and hook.

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

In Ivette, marks as unreachable the statements of functions whose body has not
been analyzed.

Sets the computation state [Computed] _after_ the domains are marked as computed:
avoids a crash from Db.Value access functions when the cvalue domain has not
been marked as computed.

[Eva] multidim: Add array segmentation for array invariants inference

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

Non-scalar lvalues are now completely ignored from the valuation, so no need
to check for empty structs or unions here.

Cvalues can only represent scalar values; they are irrelevant on structs or
arrays.

The cvalues cannot precisely represent structs and arrays: they are irrelevant
and could degrade the state precision for such lvalues.

Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago

- fixed incorrect assigns
- imprecise but correct handling of allocates
- handling imprecise assigns on sub parts of a base
- always normalize the domain by removing tops when updating the map

Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago

- Remove empty segments before bound updates so the oracle can be used
- Remove empty segments before joins and updates to improve precision
- Keep segmentation hints as long as possible
- Add comments to the test