Draft: Track default values

Since recently, calls to val-functions are executed abstractly, also in concrete execution. This means that the result of the call is just the result value from the model, if the model provides it, or the default value otherwise.

Default values are a shot in the dark regarding the postconditions, which are then likely to be wrong. A contradiction in the postcondition of an abstract call results in the RAC execution to get stuck, which results in the final verdict that the model is BAD, and the prover model is hidden.

RAC execution and the final verdict should in this case be INCOMPLETE, because it is an incompleteness of the program (missing implementation) and the model (missing value). The prover model should be retained.

With this MR, all values track their origin (from a computation, from the model, default value), and when an assumption is disproven, an exception Cannot_compute is raised instead of an exception RAC_stuck.

@cbelodas @marche One issue with this approach is that if values result from computations with parameters that are default values, it should also trigger an incompleteness (Cannot_compute) instead of a RAC_stuck. Do we have to taint values originating from computations based on default values as well?

If I understood your question correctly I would say yes. Once you take a default value it becomes difficult to detect what values are affected by the default values assumed. Or are you able to do it with the origin field you introduced?

added 9 commits

• 7327a551...42c6d820 - 2 commits from branch master
• d8732dee - Make type value abstract but expose value_desc
• e783f74e - Add field to values to track its origin
• d706947f - Get stuck when assumption fail only when no free variables has a default value
• d9db1c75 - Use boolean field to track default values
• 29c720b2 - Clean Value module
• 0de6bfdc - Propagate defaultness of values across computations
• c52a8d52 - Update oracles

Compare with previous version

changed title from Draft: Differentiate value origin to Draft: Track default values

added component: counterexample label

mentioned in merge request !424 (merged)

assigned to @bbecker

closed