GitLab

The value of bitvector can not fit into integer range (it can be, e.g,
9223372036854775881). Values of bitvectors are stored as strings and not
converted to integers.

This is to ensure the assumption of the transformation
intro_projections_counterexmp that every variable with model label has
location. For variables without location, it makes no sense to include
them in counterexample.

Record fields labeled with label model_trace:@hide_field will be not
shown in counterexample.

Previously, "." was automatically appended to names stored in
model_trace label when creating variables corresponding to record
fields in eval_match and when projecting record fields in the
transformation intro_projections_counterexmp. Now, this is not done
and "." must be given in model_trace label of the projection or
record field.

The reason is that for SPARK, character different from "." (e.g., "'"
needs to be sometimes appended.

In standard WP, propagate also location of the expression, in fast wp,
do not propagate model labels through Eany expression.

Since the exact line of the construct that triggers VC may not be
known, the possibility to map the counterexample information related
to this construct to dedicated index instead of mapping it to line
number was added.

Note that the line of the construct that triggers VC is guaranteed to
be known only if  this construct does not span to multiple lines or if
the VC is not split.

the name of the projection to projected element.

Model elements in source code line are represented as list of JSON objects
with attributes "name", "value", and "kind". The attribute "name" is a
name of a counterexample element, the attribute "value" is the value of
the counterexample element, and the attribute "kind" is the kind of
counterexample element, currently one of "old", "result", "error_message",
and "other".

Prevent loosing labels of formulas with f.t_node equal to Tquant in
transformations eliminate_algebraic and introduce_premises.

Need to compile Alt-Ergo with Nums instead of Zarith,
which is not supported by js_of_ocaml

The concatenation of strings in the list of strings returned by
bounded_split must be equal to the string being split.

Postconditions for that variables mentioned in these postconditions
should be in counterexample are now marked with label "model_vc_post".

Variables corresponding to return values are no longer handled by
transformation intro_vc_vars_counterexmp. They must have location
of the corresponding postcondition, label "model" or "model_trace", and
label of the form "model_trace:name@result". Generartion of these labels
to variables corresponding to return values created in WP is for future
work.

dans ace/src-noconflicts

needs 'ace' to run, which can be retrieved using

git clone https://github.com/ajaxorg/ace-builds.git

Do not append '.' to the name of the variable representing field access
if the field name is empty string (that is, if the field name should be
ignored in counterexample).

were added to original labels.

When eval_match creates new terms from original terms, all labels of
the original terms are copied to the new terms. The exception are
labels of the form "model_trace:*". These labels are not copied if both
original terms and new terms contain this label.

In wp, eval_match is used to replace record fields with simple variables
of the same type. Originally, all labels from the variable that field
was accessed were copied to new variables representing fields of this
variable. Therefore also "model_trace:var_name" label was copied and thus
the field had name "var_name" in the counterexample.

This commit solves this problem by appending names of the fields to
"model_trace:*" label of new variables representing record fields.