- reproduce assert behavior for invariants

Fixes a Frama-C crash in Ivette when selecting an AST element that cannot be
evaluated into an Eva value.

Maxime Jacquemin authored 3 years ago and Maxime Jacquemin committed 3 years ago

Just some minor rewritting.

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

Adds a few comments.

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

The evaluation [v_before] is now mandatory in the getValues output.
The getValues request now returns a record for each evaluation, containing:
- the resulting value as a string;
- the alarms emitted by the evaluation;
- the variables pointed to by the value, if any. This list is also computed
  when the result is an offsetmap (for struct and arrays).

Removes request [getPointedLvalues].

- `Translate_terms.term_to_exp` -> `Translate_terms.to_exp`
- `Translate_predicates.predicate_to_exp` -> `Translate_predicates.to_exp`
- `Translate_predicates.translate_predicate` -> `Translate_predicate.do_it`
- `Translate_rtes.translate_rte_annots` -> `Translate_rtes.rte_annots`
- `Translate_rtes.translate_rte` -> `Translate_rtes.exp`