Maxime Jacquemin authored 4 years ago and David Bühler committed 3 years ago

The previous way of building eval_lval and eval_exp only evaluated the
functor Make once, which is not what we want. This should be fixed.

Maxime Jacquemin authored 4 years ago and David Bühler committed 3 years ago

The evaluation could only contain unrestricted_response evaluation,
which was quite bothering as it makes the GADT useless.
I've modified it to be able to represent restricted_to_callstack
evaluation as well.
The modification is propagated to eval_lval and eval_exp.

Maxime Jacquemin authored 4 years ago and David Bühler committed 3 years ago

The new names should be clearer.
A restricted_for_callstack Response.t cannot be a Consolidated.
A unrestricted_response Response.t can be anything.

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

I've replaced the polymorphic variant with a GADT and modified what was
necessary to compile. It should have the same behaviour.

The only questionnable modification is on the type evaluation of the
Make functor. I've been forced to add a new 'callstack parameter because
Response.t has now two parameters.

Unmarshal: Hide type-breaking code behind Sys.opaque_identity

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

Lint: Unification et simplification

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

[E-ACSL] Remove unused functions

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

[tests] fix non-portable regex in test

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